SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Church encoding</title>

</head>

Church encoding

</h1>

</header>

In <a href="Mathematics" title="Mathematics">mathematics</a>, Church encoding is a way of representing various data types in the <a href="Lambda_calculus" title="Lambda calculus">lambda calculus</a>.

In the untyped lambda calculus the only primitive data type are functions, represented by lambda abstraction terms. Types that are usually considered primitive in other notations (such as integers, Booleans, pairs, lists, and tagged unions) are not natively present.

Hence the need arises to have ways to represent the data of these varying types by lambda terms, that is, by <a href="Higher-order_function" title="Higher-order function">functions</a> that are taking functions as their arguments and are returning functions as their results.

The Church numerals are a representation of the natural numbers using lambda notation. The method is named for <a href="Alonzo_Church" title="Alonzo Church">Alonzo Church</a>, who first encoded data in the lambda calculus this way. It can also be extended to represent other data types in the similar spirit.

This article might use the <a href="Lambda_calculus#Notation" title="Lambda calculus">alternative syntax</a> for lambda abstraction terms where λx.λy.λz.N is abbreviated as λxyz.N.

A straightforward implementation of Church encoding slows some access operations from <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(1)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(1)}</annotation>

</semantics>

</math><img src="./e66384bc40452c5452f33563fe0e27e803b0cc21.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.745ex; height:2.843ex;" alt="{\displaystyle O(1)}" loading="lazy"> to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle O(n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle O(n)}</annotation>

</semantics>

</math><img src="./34109fe397fdcff370079185bfdb65826cb5565a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.977ex; height:2.843ex;" alt="{\displaystyle O(n)}" loading="lazy">, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n}</annotation>

</semantics>

</math><img src="./a601995d55609f2d9f5e233e36fbe9ea26011b3b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.395ex; height:1.676ex;" alt="{\displaystyle n}" loading="lazy"> is the size of the <a href="Data_structure" title="Data structure">data structure</a>, making Church encoding impractical.<a href="#cite_note-Widemann-1">[1]</a> Research has shown that this can be addressed by targeted optimizations, but most <a href="Functional_programming" title="Functional programming">functional programming</a> languages instead expand their intermediate representations to contain <a href="Algebraic_data_type" title="Algebraic data type">algebraic data types</a>.<a href="#cite_note-2">[2]</a> Nonetheless Church encoding is often used in theoretical arguments, as it is a natural representation for partial evaluation and theorem proving.<a href="#cite_note-Widemann-1">[1]</a> Operations can be typed using <a href="Higher-ranked_type" class="mw-redirect" title="Higher-ranked type">higher-ranked types</a>,<a href="#cite_note-3">[3]</a> and primitive recursion is easily accessible.<a href="#cite_note-Widemann-1">[1]</a> The assumption that functions are the only primitive data types streamlines many proofs.

Church encoding is complete but only representationally. Additional functions are needed to translate the representation into common data types, for display to people. It is not possible in general to decide if two functions are <a href="Extensionality" title="Extensionality">extensionally</a> equal due to the <a href="Lambda_calculus#Undecidability_of_equivalence" title="Lambda calculus">undecidability of equivalence</a> from <a href="Church's_theorem" class="mw-redirect" title="Church's theorem">Church's theorem</a>. The translation may apply the function in some way to retrieve the value it represents, or look up its value as a literal lambda term. Lambda calculus is usually interpreted as using <a href="Deductive_lambda_calculus" class="mw-redirect" title="Deductive lambda calculus">intensional equality</a>. There are <a href="Deductive_lambda_calculus" class="mw-redirect" title="Deductive lambda calculus">potential problems</a> with the interpretation of results because of the difference between the intensional and extensional definition of equality.

<div class="mw-heading mw-heading2"><h2 id="Church_numerals">Church numerals</h2></div>

Church numerals are the representations of <a href="Natural_number" title="Natural number">natural numbers</a> under Church encoding. The <a href="Higher-order_function" title="Higher-order function">higher-order function</a> that represents natural number n is a function that maps any function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f}</annotation>

</semantics>

</math><img src="./132e57acb643253e7810ee9702d9581f159a1c61.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.279ex; height:2.509ex;" alt="{\displaystyle f}" loading="lazy"> to its n-fold <a href="Function_composition" title="Function composition">composition</a>. In simpler terms, a numeral represents the number by applying any given function that number of times in sequence, starting from any given starting value:

<msup>

</mrow>

</msup>

<mrow>

</mrow>

</munder>

</mrow>

<mtext> times</mtext>

</mrow>

</munder>

<mrow>

</mrow>

</munder>

</mrow>

<mtext> times</mtext>

</mrow>

</munder>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f^{\circ n}(x)=\underbrace {f\circ f\circ \ldots \circ f} _{n{\text{ times}}}\,(x)=\underbrace {f(f(\ldots (f} _{n{\text{ times}}}\,(x))\ldots ))}</annotation>

</semantics>

</math><img src="./f1f62927f018da4d2d88cbb9dc95751022821588.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -4.338ex; width:48.376ex; height:6.343ex;" alt="{\displaystyle f^{\circ n}(x)=\underbrace {f\circ f\circ \ldots \circ f} _{n{\text{ times}}}\,(x)=\underbrace {f(f(\ldots (f} _{n{\text{ times}}}\,(x))\ldots ))}" loading="lazy"></dd></dl>

All Church numerals are functions that take two parameters. Church numerals 0, 1, 2, ..., are defined as follows in the <a href="Lambda_calculus" title="Lambda calculus">lambda calculus</a>:

<dl><dd>Starting with 0 not applying the function at all, proceed with 1 applying the function once, 2 applying the function twice in a row, 3 applying the function three times in a row, etc.:</dd></dl>

<mtr>

<mtd>

<mtext>Number</mtext>

</mrow>

</mtd>

<mtd>

<mtext>Function definition</mtext>

</mrow>

</mtd>

<mtd>

<mtext>Lambda expression</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<msup>

</mrow>

</msup>

</mtd>

<mtd>

<msup>

</mrow>

</msup>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{\circ n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}</annotation>

</semantics>

</math><img src="./1f1201d277a92cbc9da12166a2a914e556bf4143.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -11.838ex; width:56.988ex; height:24.843ex;" alt="{\displaystyle {\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{\circ n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}" loading="lazy"></dd></dl>

The Church numeral 3 is a chain of three applications of any given function in sequence, starting from some value. The supplied function is first applied to a supplied argument and then successively to its own result. The end result is not the number 3 (unless the supplied parameter happens to be 0 and the function is a <a href="Successor_function" title="Successor function">successor function</a>). The function itself, and not its end result, is the Church numeral 3. The Church numeral 3 means simply to do something three times. It is an <a href="Ostensive_definition" title="Ostensive definition">ostensive</a> demonstration of what is meant by "three times".

<div class="mw-heading mw-heading3"><h3 id="Calculation_with_Church_numerals">Calculation with Church numerals</h3></div>

<a href="Arithmetic" title="Arithmetic">Arithmetic</a> operations on numbers may be represented by functions on Church numerals. These functions may be defined in <a href="Lambda_calculus" title="Lambda calculus">lambda calculus</a>, or implemented in most functional programming languages (see <a href="Lambda_lifting#Conversion_without_lifting" title="Lambda lifting">converting lambda expressions to functions</a>).

The addition function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {plus} (m,n)=m+n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {plus} (m,n)=m+n}</annotation>

</semantics>

</math><img src="./1a7e570c6c1e7637d3d5d56a40d5263cc73cb283.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.8ex; height:2.843ex;" alt="{\displaystyle \operatorname {plus} (m,n)=m+n}" loading="lazy"> uses the identity <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))}">

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))}</annotation>

</semantics>

</math><img src="./28a1e15af00b7dd76e2ce966859216bfbd316e7a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.726ex; height:3.343ex;" alt="{\displaystyle f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))}" loading="lazy">.

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {plus} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}</annotation>

</semantics>

</math><img src="./58758b6fa3ebc7f6adf7978262d9292514314018.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:34.301ex; height:2.843ex;" alt="{\displaystyle \operatorname {plus} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}" loading="lazy"></dd></dl>

The successor function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {succ} (n)=n+1}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {succ} (n)=n+1}</annotation>

</semantics>

</math><img src="./95efd954ffac3f51881898263e74d49ff0676664.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:15.974ex; height:2.843ex;" alt="{\displaystyle \operatorname {succ} (n)=n+1}" loading="lazy"> is <a href="Beta_reduction" class="mw-redirect" title="Beta reduction">β-equivalent</a> to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\operatorname {plus} \ 1)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (\operatorname {plus} \ 1)}</annotation>

</semantics>

</math><img src="./ba88e2dfbb0488466dfd249012794ed71bcd4a3e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:8.088ex; height:2.843ex;" alt="{\displaystyle (\operatorname {plus} \ 1)}" loading="lazy">.

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {succ} \equiv \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}</annotation>

</semantics>

</math><img src="./58de484d980602d2415f8acc94677952f33b78cb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.375ex; height:2.843ex;" alt="{\displaystyle \operatorname {succ} \equiv \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}" loading="lazy"></dd></dl>

The multiplication function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {mult} (m,n)=m*n}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {mult} (m,n)=m*n}</annotation>

</semantics>

</math><img src="./51269fa75fdb6f02faaafcab2ea522ed14142e9f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.787ex; height:2.843ex;" alt="{\displaystyle \operatorname {mult} (m,n)=m*n}" loading="lazy"> uses the identity <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)}">

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)}</annotation>

</semantics>

</math><img src="./14a6bcfe4e5b4e99b1df7bcb3186ad94ab854644.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:23.949ex; height:3.343ex;" alt="{\displaystyle f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)}" loading="lazy">.

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {mult} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}</annotation>

</semantics>

</math><img src="./cd7b95a40139cfaaadd4d812f57f2d52f5fc2002.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.073ex; height:2.843ex;" alt="{\displaystyle \operatorname {mult} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}" loading="lazy"></dd></dl>

The exponentiation function <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {exp} (b,n)=b^{n}}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {exp} (b,n)=b^{n}}</annotation>

</semantics>

</math><img src="./5bab7af5c7654b5974f914290766f0a5f4f1549d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.102ex; height:2.843ex;" alt="{\displaystyle \operatorname {exp} (b,n)=b^{n}}" loading="lazy"> is given by the definition of Church numerals, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n\ h\ x=h^{n}\ x}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n\ h\ x=h^{n}\ x}</annotation>

</semantics>

</math><img src="./f58c493a6a86918c26a3001572c2e7bb712fe49b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:12.791ex; height:2.343ex;" alt="{\displaystyle n\ h\ x=h^{n}\ x}" loading="lazy">. In the definition substitute <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h\to b,x\to f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h\to b,x\to f}</annotation>

</semantics>

</math><img src="./368389168a01bda8f248736e96b779c238ecd7cb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.207ex; height:2.509ex;" alt="{\displaystyle h\to b,x\to f}" loading="lazy"> to get <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n\ b\ f=b^{n}\ f}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n\ b\ f=b^{n}\ f}</annotation>

</semantics>

</math><img src="./7a88b751deeb49ce50f0e4c21960e35ef049050b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:12.006ex; height:2.676ex;" alt="{\displaystyle n\ b\ f=b^{n}\ f}" loading="lazy"> and,

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {exp} \ b\ n=b^{n}=n\ b}</annotation>

</semantics>

</math><img src="./01283ad262a449e7b0a71212ec0a2ebc76d4c1c9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:18.879ex; height:2.676ex;" alt="{\displaystyle \operatorname {exp} \ b\ n=b^{n}=n\ b}" loading="lazy"></dd></dl>

which gives the lambda expression,

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {exp} \equiv \lambda b.\lambda n.n\ b}</annotation>

</semantics>

</math><img src="./c0c9b44f863cd423d1ba9e78f4ded7eaa27b546f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:16.794ex; height:2.509ex;" alt="{\displaystyle \operatorname {exp} \equiv \lambda b.\lambda n.n\ b}" loading="lazy"></dd></dl>

The <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {pred} (n)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {pred} (n)}</annotation>

</semantics>

</math><img src="./cc7c43daf72dac334ebcba6835120653414e096a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.733ex; height:2.843ex;" alt="{\displaystyle \operatorname {pred} (n)}" loading="lazy"> function is more difficult to understand.

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}</annotation>

</semantics>

</math><img src="./9e8fbc0ac6a7f712a0f47d06e59de9aa113f9f5b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:51.397ex; height:2.843ex;" alt="{\displaystyle \operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}" loading="lazy"></dd></dl>

A Church numeral applies a function n times. The predecessor function must return a function that applies its parameter n - 1 times. This is achieved by building a container around f and x, which is initialized in a way that omits the application of the function the first time. See <a href="#Derivation_of_predecessor_function">predecessor</a> for a more detailed explanation.

The subtraction function can be written based on the predecessor function.

<mi>minus</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {minus} \equiv \lambda m.\lambda n.(n\operatorname {pred} )\ m}</annotation>

</semantics>

</math><img src="./f0c99c5f1f220a1c40885e1eae32b2be222fc3ef.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:28.137ex; height:2.843ex;" alt="{\displaystyle \operatorname {minus} \equiv \lambda m.\lambda n.(n\operatorname {pred} )\ m}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Table_of_functions_on_Church_numerals">Table of functions on Church numerals</h3></div>

<th>Function</th>

<th>Algebra</th>

<th>Identity</th>

<th>Function definition

</th>

<th colspan="2">Lambda expressions

</th></tr>

<tr>

<td><a href="Successor_function" title="Successor function">Successor</a></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n+1}</annotation>

</semantics>

</math><img src="./2a135e65a42f2d73cccbfc4569523996ca0036f1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.398ex; height:2.343ex;" alt="{\displaystyle n+1}" loading="lazy"></td>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f^{n+1}\ x=f(f^{n}x)}</annotation>

</semantics>

</math><img src="./28c139dca219d67a2a2a586bee3d2911fe67643e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.605ex; height:3.176ex;" alt="{\displaystyle f^{n+1}\ x=f(f^{n}x)}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)}</annotation>

</semantics>

</math><img src="./39b0e0450edefefa60cbbf51a40e7a798c4af186.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:22.337ex; height:2.843ex;" alt="{\displaystyle \operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}</annotation>

</semantics>

</math><img src="./d6df54b2670776a76cb587d02cde997185cea574.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.003ex; height:2.843ex;" alt="{\displaystyle \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}" loading="lazy"></td>

<td>...

</td></tr>

<tr>

<td><a href="Addition" title="Addition">Addition</a></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m+n}</annotation>

</semantics>

</math><img src="./88528fefcfac1b22d2df9b71d0f4fc9e758f65ad.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.276ex; height:2.176ex;" alt="{\displaystyle m+n}" loading="lazy"></td>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f^{m+n}\ x=f^{m}(f^{n}x)}</annotation>

</semantics>

</math><img src="./686960f2c228d0dabb006509436ce5a5c5fef28d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.943ex; height:3.009ex;" alt="{\displaystyle f^{m+n}\ x=f^{m}(f^{n}x)}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {plus} \ m\ n\ f\ x=m\ f\ (n\ f\ x)}</annotation>

</semantics>

</math><img src="./f9fce325ca66d7a7386cbe61f311dcbbb95c4b00.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.454ex; height:2.843ex;" alt="{\displaystyle \operatorname {plus} \ m\ n\ f\ x=m\ f\ (n\ f\ x)}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}</annotation>

</semantics>

</math><img src="./a4896eac77eda812f3df91610deabcc9e085ab04.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.054ex; height:2.843ex;" alt="{\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda m.\lambda n.n\operatorname {succ} m}</annotation>

</semantics>

</math><img src="./5b3b42b6c60b0bc5acdfc6162c53dee2db080182.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:16.696ex; height:2.176ex;" alt="{\displaystyle \lambda m.\lambda n.n\operatorname {succ} m}" loading="lazy">

</td></tr>

<tr>

<td><a href="Multiplication" title="Multiplication">Multiplication</a></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m*n}</annotation>

</semantics>

</math><img src="./1ffcd7d554b97eb5775db68e72e8f0274fe38713.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.63ex; height:1.676ex;" alt="{\displaystyle m*n}" loading="lazy"></td>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f^{m*n}\ x=(f^{m})^{n}\ x}</annotation>

</semantics>

</math><img src="./0b97082911871e9828ccc6417d0a30641c142da0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.746ex; height:2.843ex;" alt="{\displaystyle f^{m*n}\ x=(f^{m})^{n}\ x}" loading="lazy"></td>

<mi>multiply</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x}</annotation>

</semantics>

</math><img src="./6ab6808052395bf73bc7c57eceb5aaaff0fa4a41.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.04ex; height:2.843ex;" alt="{\displaystyle \operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}</annotation>

</semantics>

</math><img src="./41f860ea07d1c9899605d98430fd3fec5ebe225f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.195ex; height:2.843ex;" alt="{\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda m.\lambda n.\lambda f.m\ (n\ f)}</annotation>

</semantics>

</math><img src="./cd6d4236bb601746e908342999b515fb2b3adb5d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.565ex; height:2.843ex;" alt="{\displaystyle \lambda m.\lambda n.\lambda f.m\ (n\ f)}" loading="lazy">

</td></tr>

<tr>

<td><a href="Exponentiation" title="Exponentiation">Exponentiation</a></td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle b^{n}}</annotation>

</semantics>

</math><img src="./b8f8f52cd26bb201e02c8d1b3619a3a682f44dbc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.216ex; height:2.343ex;" alt="{\displaystyle b^{n}}" loading="lazy"></td>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n\ b\ f=b^{n}\ f}</annotation>

</semantics>

</math><img src="./7a88b751deeb49ce50f0e4c21960e35ef049050b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:12.006ex; height:2.676ex;" alt="{\displaystyle n\ b\ f=b^{n}\ f}" loading="lazy"><a href="#cite_note-Church_numeral_definition-4">[a]</a></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {exp} \ b\ n\ f\ x=n\ b\ f\ x}</annotation>

</semantics>

</math><img src="./596cc481d72b24e627d85a52f48d7042973759e1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:21.104ex; height:2.509ex;" alt="{\displaystyle \operatorname {exp} \ b\ n\ f\ x=n\ b\ f\ x}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda b.\lambda n.\lambda f.\lambda x.n\ b\ f\ x}</annotation>

</semantics>

</math><img src="./9ed541e07e3ebd9d7ba7fc7106c5b1250393e87e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:21.3ex; height:2.509ex;" alt="{\displaystyle \lambda b.\lambda n.\lambda f.\lambda x.n\ b\ f\ x}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda b.\lambda n.n\ b}</annotation>

</semantics>

</math><img src="./17deda669ff2513ad12d97ecce3ccfa3c3597360.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.144ex; height:2.176ex;" alt="{\displaystyle \lambda b.\lambda n.n\ b}" loading="lazy">

</td></tr>

<tr>

<td><a href="#Derivation_of_predecessor_function">Predecessor</a><a href="#cite_note-ce-5">[b]</a></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n-1}</annotation>

</semantics>

</math><img src="./fbd0b0f32b28f51962943ee9ede4fb34198a2521.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.398ex; height:2.343ex;" alt="{\displaystyle n-1}" loading="lazy"></td>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {inc} ^{n}\operatorname {con} =\operatorname {val} (f^{n-1}x)}</annotation>

</semantics>

</math><img src="./66427efa0f1b28d5d29eb193eee6141cc2382c0b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.978ex; height:3.176ex;" alt="{\displaystyle \operatorname {inc} ^{n}\operatorname {con} =\operatorname {val} (f^{n-1}x)}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {if} (n==0)\ 0\ \operatorname {else} \ (n-1)}</annotation>

</semantics>

</math><img src="./09cdf142a30fabb09e8fa143f73f47473ed51095.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.145ex; height:2.843ex;" alt="{\displaystyle \operatorname {if} (n==0)\ 0\ \operatorname {else} \ (n-1)}" loading="lazy">

</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}</annotation>

</semantics>

</math><img src="./322777a401ea0b46986d17ab947cbe1391bd95b1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:43.77ex; height:2.843ex;" alt="{\displaystyle \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}" loading="lazy">

</td></tr>

<tr>

<td><a href="Subtraction" title="Subtraction">Subtraction</a><a href="#cite_note-ce-5">[b]</a> (<a href="Monus" title="Monus">Monus</a>)</td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m-n}</annotation>

</semantics>

</math><img src="./767c4b0c3cbd063f836169c2db77f5ffd833d136.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.276ex; height:2.176ex;" alt="{\displaystyle m-n}" loading="lazy"></td>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f^{m-n}\ x=(f^{-1})^{n}(f^{m}x)}</annotation>

</semantics>

</math><img src="./c647fa4b2544bc24301fbe7507ff4e507f5cc2ea.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:23.085ex; height:3.176ex;" alt="{\displaystyle f^{m-n}\ x=(f^{-1})^{n}(f^{m}x)}" loading="lazy"></td>

<mi>minus</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {minus} \ m\ n=(n\operatorname {pred} )\ m}</annotation>

</semantics>

</math><img src="./fce5e92bc332548332d464ccdbf7c6ae67785895.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.907ex; height:2.843ex;" alt="{\displaystyle \operatorname {minus} \ m\ n=(n\operatorname {pred} )\ m}" loading="lazy"></td>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda m.\lambda n.n\operatorname {pred} m}</annotation>

</semantics>

</math><img src="./ce72961d1e7ab40a5883ac558e1e9b7641a4de17.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:16.952ex; height:2.509ex;" alt="{\displaystyle \lambda m.\lambda n.n\operatorname {pred} m}" loading="lazy">

</td></tr></tbody></table>

Notes: <style data-mw-deduplicate="TemplateStyles:r1239543626">

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist reflist-lower-alpha">

<li id="cite_note-Church_numeral_definition-4"><a href="#cite_ref-Church_numeral_definition_4-0">^</a> This formula is the definition of a Church numeral n with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle f\to b,x\to f}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle f\to b,x\to f}</annotation>

</semantics>

</math><img src="./3fde9168cb836420eb1f9c4f6cf148eaa2c407d0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.146ex; height:2.509ex;" alt="{\displaystyle f\to b,x\to f}" loading="lazy">.

</li>

<li id="cite_note-ce-5">^ <a href="#cite_ref-ce_5-0">a</a> <a href="#cite_ref-ce_5-1">b</a> In the Church encoding,

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {pred} (0)=0}</annotation>

</semantics>

</math><img src="./97760225e16261b4333c6e317dfbb6a3ee1270af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.762ex; height:2.843ex;" alt="{\displaystyle \operatorname {pred} (0)=0}" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m\leq n\to m-n=0}</annotation>

</semantics>

</math><img src="./cbdce4a12934c09525aa31b97087cb8e2a128682.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:20.684ex; height:2.343ex;" alt="{\displaystyle m\leq n\to m-n=0}" loading="lazy"></li></ul>

</li>

</ol></div></div>

<div class="mw-heading mw-heading3"><h3 id="Derivation_of_predecessor_function">Derivation of predecessor function</h3></div>

The predecessor function used in the Church encoding is,

<mrow>

<mtr>

<mtd>

</mtd>

<mtd>

</mstyle>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mtext>otherwise</mtext>

</mstyle>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}}</annotation>

</semantics>

</math><img src="./22a6f84572b2bd98ae772554c94b6fea7bfdf1b2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:30.623ex; height:6.176ex;" alt="{\displaystyle \operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}}" loading="lazy">.</dd></dl>

We need a way of applying the function 1 fewer times to build the predecessor. A numeral n applies the function f n times to x. The predecessor function must use the numeral n to apply the function n-1 times.

Before implementing the predecessor function, here is a scheme that wraps the value in a container function. We will define new functions to use in place of f and x, called inc and init. The container function is called value. The left-hand side of the table shows a numeral n applied to inc and init.

<mtr>

<mtd>

<mtext>Number</mtext>

</mrow>

</mtd>

<mtd>

<mtext>Using init</mtext>

</mrow>

</mtd>

<mtd>

<mtext>Using const</mtext>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>value</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>value</mi>

</mtd>

<mtd>

<mi>const</mi>

<mi>value</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>value</mi>

</mtd>

<mtd>

<mi>const</mi>

<mi>value</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>value</mi>

</mtd>

<mtd>

<mi>const</mi>

<mi>value</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>value</mi>

<msup>

</mrow>

</msup>

<mi>value</mi>

</mtd>

<mtd>

<mi>const</mi>

<mi>value</mi>

<msup>

</mrow>

</msup>

<mi>value</mi>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{array}{r|r|r}{\text{Number}}&{\text{Using init}}&{\text{Using const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)&\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x\\2&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}}</annotation>

</semantics>

</math><img src="./f0a8fa4d4450712b4bdf2b0d5d446313036b65dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -12.005ex; width:108.567ex; height:25.176ex;" alt="{\displaystyle {\begin{array}{r|r|r}{\text{Number}}&{\text{Using init}}&{\text{Using const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)&\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x\\2&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}}" loading="lazy"></dd></dl>

The general recurrence rule is,

<mi>value</mi>

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}</annotation>

</semantics>

</math><img src="./e886b3635401328c84071097e496f537f33452ce.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.43ex; height:2.843ex;" alt="{\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}" loading="lazy"></dd></dl>

If there is also a function to retrieve the value from the container (called extract),

<mi>extract</mi>

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {extract} \ (\operatorname {value} \ v)=v}</annotation>

</semantics>

</math><img src="./422c6f840a8e0eb7706581cc514c58188c327e1d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.636ex; height:2.843ex;" alt="{\displaystyle \operatorname {extract} \ (\operatorname {value} \ v)=v}" loading="lazy"></dd></dl>

Then extract may be used to define the samenum function as,

<mi>samenum</mi>

<mi>extract</mi>

<mi>extract</mi>

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n}</annotation>

</semantics>

</math><img src="./0ea51765971ac69a676b5408aa957b454b3d6872.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:107.656ex; height:2.843ex;" alt="{\displaystyle \operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n}" loading="lazy"></dd></dl>

The samenum function is not intrinsically useful. However, as inc delegates calling of f to its container argument, we can arrange that on the first application inc receives a special container that ignores its argument allowing to skip the first application of f. Call this new initial container const. The right-hand side of the above table shows the expansions of n inc const. Then by replacing init with const in the expression for the same function we get the predecessor function,

<mi>extract</mi>

<mi>const</mi>

<mi>extract</mi>

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)}</annotation>

</semantics>

</math><img src="./7f7c4c9afdf30a845f6f03a72366e2f22414d68c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:121.871ex; height:2.843ex;" alt="{\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)}" loading="lazy"></dd></dl>

As explained below the functions inc, init, const, value and extract may be defined as,

<mtr>

<mtd>

<mi>value</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>extract</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>const</mi>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}}</annotation>

</semantics>

</math><img src="./f8a082481237c7c95a7fb1d70155b4c859ce9d9a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.005ex; width:26.561ex; height:15.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}}" loading="lazy"></dd></dl>

Which gives the lambda expression for pred as,

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}</annotation>

</semantics>

</math><img src="./577c98ece78f9ea7acf051d345afce813767caf4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:51.397ex; height:2.843ex;" alt="{\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading4"><h4 id="Value_container">Value container</h4></div>

The value container applies a function to its value. It is defined by,

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {value} \ v\ h=h\ v}</annotation>

</semantics>

</math><img src="./296394d31adf4b7df3fcb4b0f4944783aa45fe95.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:15.522ex; height:2.176ex;" alt="{\displaystyle \operatorname {value} \ v\ h=h\ v}" loading="lazy"></dd></dl>

so,

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {value} =\lambda v.(\lambda h.h\ v)}</annotation>

</semantics>

</math><img src="./c1e9c5d4dc96a07741aca02ec6bb6134431ff6c5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.562ex; height:2.843ex;" alt="{\displaystyle \operatorname {value} =\lambda v.(\lambda h.h\ v)}" loading="lazy"></dd></dl>

The inc function should take a value containing v, and return a new value containing f v.

<mi>value</mi>

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}</annotation>

</semantics>

</math><img src="./e886b3635401328c84071097e496f537f33452ce.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.43ex; height:2.843ex;" alt="{\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}" loading="lazy"></dd></dl>

Letting g be the value container,

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g=\operatorname {value} \ v}</annotation>

</semantics>

</math><img src="./cdab438c5bc71e8f4467643dd444ba4bd4a3e205.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:11.672ex; height:2.509ex;" alt="{\displaystyle g=\operatorname {value} \ v}" loading="lazy"></dd></dl>

then,

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle g\ f=\operatorname {value} \ v\ f=f\ v}</annotation>

</semantics>

</math><img src="./6aac244facfe7824d577b59ed4430e0bd80506e0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:21.475ex; height:2.509ex;" alt="{\displaystyle g\ f=\operatorname {value} \ v\ f=f\ v}" loading="lazy"></dd></dl>

so,

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {inc} \ g=\operatorname {value} \ (g\ f)}</annotation>

</semantics>

</math><img src="./ca5a265845bc1b00b5dc1d464513b74d63e6a25c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.268ex; height:2.843ex;" alt="{\displaystyle \operatorname {inc} \ g=\operatorname {value} \ (g\ f)}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)}</annotation>

</semantics>

</math><img src="./08e61fa52f32837ea9613ecce65eeb4bf6df30de.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.008ex; height:2.843ex;" alt="{\displaystyle \operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)}" loading="lazy"></dd></dl>

</td>

<div class="mw-heading mw-heading4"><h4 id="Extract">Extract</h4></div>

The value may be extracted by applying the identity function,

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle I=\lambda u.u}</annotation>

</semantics>

</math><img src="./63d437eb0828936d905b53f50c7de25f8eec99a8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:9.319ex; height:2.176ex;" alt="{\displaystyle I=\lambda u.u}" loading="lazy"></dd></dl>

Using I,

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {value} \ v\ I=v}</annotation>

</semantics>

</math><img src="./1068700c1f04f1bcc35076c6e3c1605b75b6069d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:13.436ex; height:2.176ex;" alt="{\displaystyle \operatorname {value} \ v\ I=v}" loading="lazy"></dd></dl>

so,

<mi>extract</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {extract} \ k=k\ I}</annotation>

</semantics>

</math><img src="./0085ea74f6633100ea49a02cc8eb14e534081af1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:15.417ex; height:2.176ex;" alt="{\displaystyle \operatorname {extract} \ k=k\ I}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading4"><h4 id="Const">Const</h4></div>

To implement pred the init function is replaced with the const that does not apply f. We need const to satisfy,

<mi>const</mi>

<mi>value</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x}</annotation>

</semantics>

</math><img src="./0c6833719871ae14f7903fcab8396fac50d73fbd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:20.392ex; height:2.176ex;" alt="{\displaystyle \operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x}" loading="lazy"></dd>

<mi>const</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x}</annotation>

</semantics>

</math><img src="./ec90a2b09851f80974e3789cbecc5ff39993027a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.088ex; height:2.843ex;" alt="{\displaystyle \lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x}" loading="lazy"></dd></dl>

Which is satisfied if,

<mi>const</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {const} \ f=x}</annotation>

</semantics>

</math><img src="./bb5e096119d14f231512d0c2f547e4cb4d48d7be.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:11.983ex; height:2.509ex;" alt="{\displaystyle \operatorname {const} \ f=x}" loading="lazy"></dd></dl>

Or as a lambda expression,

<mi>const</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {const} =\lambda u.x}</annotation>

</semantics>

</math><img src="./f087ed9a82ff570f96f73876bccd7f1478ca4ba6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:13.455ex; height:2.176ex;" alt="{\displaystyle \operatorname {const} =\lambda u.x}" loading="lazy"></dd></dl>

</td></tr></tbody></table>

<div class="mw-heading mw-heading4"><h4 id="Another_explanation_of_pred">Another explanation of pred</h4></div>

A much simpler presentation is enabled using combinators notation.

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Kxy=x}</annotation>

</semantics>

</math><img src="./fae79da8bedad474e2a392ecdc433b8e6ad545f3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:8.979ex; height:2.509ex;" alt="{\displaystyle Kxy=x}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Ix=x}</annotation>

</semantics>

</math><img src="./5c48900bf8cf1d5bbc5dbaef706852e32770dda2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.93ex; height:2.176ex;" alt="{\displaystyle Ix=x}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Xfri=i(rf)}</annotation>

</semantics>

</math><img src="./478a8f0d6f6d680bb50dcf4d5b1e22739d1c9717.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:13.147ex; height:2.843ex;" alt="{\displaystyle Xfri=i(rf)}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred\ nfx=n(Xf)(Kx)I}</annotation>

</semantics>

</math><img src="./865c4c7b8c7e1bc862937ac9de7ac1a307a2aee8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:25.615ex; height:2.843ex;" alt="{\displaystyle Pred\ nfx=n(Xf)(Kx)I}" loading="lazy"></dd></dl>

Now it is easy enough to see that

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred\ (Succ\ n)fx=Succ\ n(Xf)(Kx)I=Xf(n(Xf)(Kx))I}</annotation>

</semantics>

</math><img src="./147541eab6f3a62d0152e8067f9b0949d76a0118.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:59.276ex; height:2.843ex;" alt="{\displaystyle Pred\ (Succ\ n)fx=Succ\ n(Xf)(Kx)I=Xf(n(Xf)(Kx))I}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \ \ \ \ =I(n(Xf)(Kx)f)=\ ...\ =I(f(f...(f(Kxf))...))=I(nfx)=nfx}</annotation>

</semantics>

</math><img src="./9477d627c3fb170755cd3acf2a44977b39c7d946.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:72.115ex; height:2.843ex;" alt="{\displaystyle \ \ \ \ =I(n(Xf)(Kx)f)=\ ...\ =I(f(f...(f(Kxf))...))=I(nfx)=nfx}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred\ Zero\ fx=\ Zero(Xf)(Kx)I=\ KxI=\ x=\ Zero\ fx}</annotation>

</semantics>

</math><img src="./0c5cf460b0b10ce05b0b294a6d939d427fbdc680.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:58.93ex; height:2.843ex;" alt="{\displaystyle Pred\ Zero\ fx=\ Zero(Xf)(Kx)I=\ KxI=\ x=\ Zero\ fx}" loading="lazy"></dd></dl>

i.e. by eta-contraction, and then by induction,

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred\ (Succ\ n)=n}</annotation>

</semantics>

</math><img src="./75cd21b9d35dd15fc769884323939afbcefa3d43.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:18.795ex; height:2.843ex;" alt="{\displaystyle Pred\ (Succ\ n)=n}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred\ Zero=Zero}</annotation>

</semantics>

</math><img src="./c42e16b2644ba40614af6db63f2905c31715016a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:18.653ex; height:2.176ex;" alt="{\displaystyle Pred\ Zero=Zero}" loading="lazy"></dd>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle Pred\ (Pred\ Zero)=\ Pred\ Zero=\ Zero}</annotation>

</semantics>

</math><img src="./dd2485552171e9b7f010daa4e7093e63f7123ff4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:41.01ex; height:2.843ex;" alt="{\displaystyle Pred\ (Pred\ Zero)=\ Pred\ Zero=\ Zero}" loading="lazy"></dd></dl>

etc.

<div class="mw-heading mw-heading4"><h4 id="Another_way_of_defining_pred">Another way of defining pred</h4></div>

Pred may also be defined using pairs:

<mtr>

<mtd>

</mtd>

<mtd>

<mi>second</mi>

<mi>second</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>first</mi>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}}</annotation>

</semantics>

</math><img src="./b68441c5fd16462aa205c3dc80b7d64f584b9fdc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -5.505ex; width:46.803ex; height:12.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}}" loading="lazy"></dd></dl>

This is a simpler definition but leads to a more complex expression for pred.

The expansion for <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {pred} \operatorname {three} }">

<mi>three</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {pred} \operatorname {three} }</annotation>

</semantics>

</math><img src="./cb8e66cbd053ff8ccd78ab38ba2c5175f51b7bf4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:10.09ex; height:2.509ex;" alt="{\displaystyle \operatorname {pred} \operatorname {three} }" loading="lazy">:

<mtr>

<mtd>

<mi>three</mi>

</mtd>

<mtd>

<mi>first</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>first</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>first</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>first</mi>

<mi>three</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {pred} \operatorname {three} =&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} ))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {one} )))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {one} \ \operatorname {two} ))\\=&\ \operatorname {first} \ (\operatorname {pair} \ \operatorname {two} \ \operatorname {three} )\\=&\ \operatorname {two} \end{aligned}}}</annotation>

</semantics>

</math><img src="./3f41ba4b30f4180fc2a5f839161526d11550a7c7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.171ex; width:47.058ex; height:15.509ex;" alt="{\displaystyle {\begin{aligned}\operatorname {pred} \operatorname {three} =&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} ))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {one} )))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {one} \ \operatorname {two} ))\\=&\ \operatorname {first} \ (\operatorname {pair} \ \operatorname {two} \ \operatorname {three} )\\=&\ \operatorname {two} \end{aligned}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Division">Division</h3></div>

<a href="Division_(mathematics)" title="Division (mathematics)">Division</a> of natural numbers may be implemented by,<a href="#cite_note-6">[4]</a>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0}</annotation>

</semantics>

</math><img src="./ed372cc30e5079bcc6fb23e8d30738b10a5a033b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:45.03ex; height:2.843ex;" alt="{\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0}" loading="lazy"></dd></dl>

Calculating <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n-m}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n-m}</annotation>

</semantics>

</math><img src="./3a9677b812ea9ee4d4538767f9aef960c69aca59.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.276ex; height:2.176ex;" alt="{\displaystyle n-m}" loading="lazy"> takes many beta reductions. Unless doing the reduction by hand, this doesn't matter that much, but it is preferable to not have to do this calculation twice. The simplest predicate for testing numbers is IsZero so consider the condition.

<mi>IsZero</mi>

<mi>minus</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}</annotation>

</semantics>

</math><img src="./2e50410a6ade27f0719b9f2fc863545efa2f2a28.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.127ex; height:2.843ex;" alt="{\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}" loading="lazy"></dd></dl>

But this condition is equivalent to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n\leq m}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n\leq m}</annotation>

</semantics>

</math><img src="./1be80a749be067190db51891139a12d4886fc054.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:6.534ex; height:2.176ex;" alt="{\displaystyle n\leq m}" loading="lazy">, not <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n<m}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n<m}</annotation>

</semantics>

</math><img src="./5cff096773597d7223f9d90162eb2d780dfc18dc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.534ex; height:1.843ex;" alt="{\displaystyle n<m}" loading="lazy">. If this expression is used then the mathematical definition of division given above is translated into function on Church numerals as,

<mi>divide1</mi>

<mi>IsZero</mi>

<mi>divide1</mi>

<mi>minus</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}</annotation>

</semantics>

</math><img src="./d71db547eae214fe79bb6ba7399e8bedf6aa92cb.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:75.746ex; height:2.843ex;" alt="{\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}" loading="lazy"></dd></dl>

As desired, this definition has a single call to <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {minus} \ n\ m}">

<mi>minus</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {minus} \ n\ m}</annotation>

</semantics>

</math><img src="./dd6752ba2f35b6bb117414c86a8e54b52cc5ff3d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:11.068ex; height:2.176ex;" alt="{\displaystyle \operatorname {minus} \ n\ m}" loading="lazy">. However the result is that this formula gives the value of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (n-1)/m}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (n-1)/m}</annotation>

</semantics>

</math><img src="./c2503ae079658383f112eda3813ebdf612579605.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.41ex; height:2.843ex;" alt="{\displaystyle (n-1)/m}" loading="lazy">.

This problem may be corrected by adding 1 to n before calling divide. The definition of divide is then,

<mi>divide</mi>

<mi>divide1</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)}</annotation>

</semantics>

</math><img src="./c3fb26928c830538b603dd4b0268462be30075a3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:28.314ex; height:2.843ex;" alt="{\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)}" loading="lazy"></dd></dl>

divide1 is a recursive definition. The <a href="Fixed-point_combinator" title="Fixed-point combinator">Y combinator</a> may be used to implement the recursion. Create a new function called div by;

<mi>divide1</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {divide1} \rightarrow \operatorname {div} \ c}</annotation>

</semantics>

</math><img src="./a5103e8f2ac076b005672dae9992e83349b4aa62.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:16.057ex; height:2.176ex;" alt="{\displaystyle \operatorname {divide1} \rightarrow \operatorname {div} \ c}" loading="lazy"></li>

<li>In the right hand side <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {divide1} \rightarrow c}">

<mi>divide1</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {divide1} \rightarrow c}</annotation>

</semantics>

</math><img src="./2baca1d16c5c9ddb17d6506bed7e86751b846c01.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:11.922ex; height:2.176ex;" alt="{\displaystyle \operatorname {divide1} \rightarrow c}" loading="lazy"></li></ul>

to get,

<mi>IsZero</mi>

<mi>minus</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}</annotation>

</semantics>

</math><img src="./6e57208acfcc292d0b50a5975eec4aa54c73ac28.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:75.174ex; height:2.843ex;" alt="{\displaystyle \operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}" loading="lazy"></dd></dl>

Then,

<mi>divide</mi>

<mi>divide1</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)}</annotation>

</semantics>

</math><img src="./7897298aa0f87ba2fbe70635f94d37dbf6c25b27.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:29.735ex; height:2.843ex;" alt="{\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)}" loading="lazy"></dd></dl>

where,

<mtr>

<mtd>

<mi>divide1</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>IsZero</mi>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}</annotation>

</semantics>

</math><img src="./b8fc6dd9dfcf2e01e934ae3038393bb761e2e9da.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.005ex; width:40.273ex; height:15.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}" loading="lazy">

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>false</mi>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}</annotation>

</semantics>

</math><img src="./d39bc19720586d643dd1923cd9e054b1614725f9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.338ex; width:16.555ex; height:5.843ex;" alt="{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}" loading="lazy"></dd></dl></dd>

<mtr>

<mtd>

<mi>minus</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}</annotation>

</semantics>

</math><img src="./8256791d68d145ea9fb99662b8030da448eaa0aa.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.338ex; width:53.704ex; height:5.843ex;" alt="{\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}" loading="lazy"></dd></dl>

Gives,

<mi>divide</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)}</annotation>

</semantics>

</math><img src="./481d17bf51a11fb45e0c8dc1f8bbccb2ab1ff1de.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:157.455ex; height:2.176ex;" alt="{\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)}" loading="lazy"></dd></dl>

Or as text, using \ for λ,

<pre>divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))

</pre>

For example, 9/3 is represented by

<pre>divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))

</pre>

Using a lambda calculus calculator, the above expression reduces to 3, using normal order.

<pre>\f.\x.f (f (f (x)))

</pre>

<div class="mw-heading mw-heading3"><h3 id="Signed_numbers">Signed numbers</h3></div>

One simple approach for extending Church Numerals to <a href="Integer" title="Integer">signed numbers</a> is to use a Church pair, containing Church numerals representing a positive and a negative value.<a href="#cite_note-7">[5]</a> The integer value is the difference between the two Church numerals.

A natural number is converted to a signed number by,

<msub>

<mi>convert</mi>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0}</annotation>

</semantics>

</math><img src="./ff7252f5290e1b2a017f1b77a818e79635fc1b88.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:23.438ex; height:2.509ex;" alt="{\displaystyle \operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0}" loading="lazy"></dd></dl>

Negation is performed by swapping the values.

<msub>

</mrow>

</msub>

<mi>second</mi>

<mi>first</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}</annotation>

</semantics>

</math><img src="./dc12867792d12bab4622295a06a22eb98ff1de60.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:35.903ex; height:2.843ex;" alt="{\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}" loading="lazy"></dd></dl>

The integer value is more naturally represented if one of the pair is zero. The OneZero function achieves this condition,

<mi>OneZero</mi>

<mi>IsZero</mi>

<mi>first</mi>

<mi>IsZero</mi>

<mi>second</mi>

<mi>OneZero</mi>

<mi>first</mi>

<mi>second</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}</annotation>

</semantics>

</math><img src="./ca6ee4ebffddbbab5cef46a534b2fe8f1a7240bc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:108.256ex; height:2.843ex;" alt="{\displaystyle \operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}" loading="lazy"></dd></dl>

The recursion may be implemented using the Y combinator,

<mi>IsZero</mi>

<mi>first</mi>

<mi>IsZero</mi>

<mi>second</mi>

<mi>first</mi>

<mi>second</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}</annotation>

</semantics>

</math><img src="./c45c693a5362d92d87ac907917dce4cae41ce190.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:100.505ex; height:2.843ex;" alt="{\displaystyle \operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}" loading="lazy"></dd></dl>

<mi>OneZero</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {OneZero} =Y\operatorname {OneZ} }</annotation>

</semantics>

</math><img src="./97ddb9de38a6efad13783dcdeacde6914863ee5b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:19.472ex; height:2.176ex;" alt="{\displaystyle \operatorname {OneZero} =Y\operatorname {OneZ} }" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Plus_and_minus">Plus and minus</h3></div>

Addition is defined mathematically on the pair by,

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x+y=[x_{p},x_{n}]+[y_{p},y_{n}]=x_{p}-x_{n}+y_{p}-y_{n}=(x_{p}+y_{p})-(x_{n}+y_{n})=[x_{p}+y_{p},x_{n}+y_{n}]}</annotation>

</semantics>

</math><img src="./724b32508d430b8bf7fd7cb05d5077473e842952.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:91.857ex; height:3.009ex;" alt="{\displaystyle x+y=[x_{p},x_{n}]+[y_{p},y_{n}]=x_{p}-x_{n}+y_{p}-y_{n}=(x_{p}+y_{p})-(x_{n}+y_{n})=[x_{p}+y_{p},x_{n}+y_{n}]}" loading="lazy"></dd></dl>

The last expression is translated into lambda calculus as,

<msub>

</mrow>

</msub>

<mi>OneZero</mi>

<mi>first</mi>

<mi>first</mi>

<mi>second</mi>

<mi>second</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))}</annotation>

</semantics>

</math><img src="./bcccb69fc34e0465e318844fecdd2f3c48423be0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:85.242ex; height:2.843ex;" alt="{\displaystyle \operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))}" loading="lazy"></dd></dl>

Similarly subtraction is defined,

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x-y=[x_{p},x_{n}]-[y_{p},y_{n}]=x_{p}-x_{n}-y_{p}+y_{n}=(x_{p}+y_{n})-(x_{n}+y_{p})=[x_{p}+y_{n},x_{n}+y_{p}]}</annotation>

</semantics>

</math><img src="./28d52c9fc0c41fe5d8b8b6e6b25607cea881fe25.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:91.857ex; height:3.009ex;" alt="{\displaystyle x-y=[x_{p},x_{n}]-[y_{p},y_{n}]=x_{p}-x_{n}-y_{p}+y_{n}=(x_{p}+y_{n})-(x_{n}+y_{p})=[x_{p}+y_{n},x_{n}+y_{p}]}" loading="lazy"></dd></dl>

giving,

<msub>

<mi>minus</mi>

</mrow>

</msub>

<mi>OneZero</mi>

<mi>first</mi>

<mi>second</mi>

<mi>second</mi>

<mi>first</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}</annotation>

</semantics>

</math><img src="./34eb7d12f12afadda5085e00695b1c5424b4e7b6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:87.178ex; height:2.843ex;" alt="{\displaystyle \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Multiply_and_divide">Multiply and divide</h3></div>

Multiplication may be defined by,

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x*y=[x_{p},x_{n}]*[y_{p},y_{n}]=(x_{p}-x_{n})*(y_{p}-y_{n})=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]}</annotation>

</semantics>

</math><img src="./f89b32d72e0682b6dd2be8ad2333f7b2b9833db9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:130.082ex; height:3.009ex;" alt="{\displaystyle x*y=[x_{p},x_{n}]*[y_{p},y_{n}]=(x_{p}-x_{n})*(y_{p}-y_{n})=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]}" loading="lazy"></dd></dl>

The last expression is translated into lambda calculus as,

<msub>

</mrow>

</msub>

<mi>first</mi>

<mi>first</mi>

<mi>second</mi>

<mi>second</mi>

<mi>first</mi>

<mi>second</mi>

<mi>second</mi>

<mi>first</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}</annotation>

</semantics>

</math><img src="./37a910b6bd661d5dcb93529bdd1a9caf42192050.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:144.705ex; height:2.843ex;" alt="{\displaystyle \operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}" loading="lazy"></dd></dl>

A similar definition is given here for division, except in this definition, one value in each pair must be zero (see OneZero above). The divZ function allows us to ignore the value that has a zero component.

<mi>IsZero</mi>

<mi>divide</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)}</annotation>

</semantics>

</math><img src="./d4378dbd52a1eff399c20edb33473c55f9dabecc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:37.66ex; height:2.843ex;" alt="{\displaystyle \operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)}" loading="lazy"></dd></dl>

divZ is then used in the following formula, which is the same as for multiplication, but with mult replaced by divZ.

<msub>

<mi>divide</mi>

</mrow>

</msub>

<mi>first</mi>

<mi>first</mi>

<mi>second</mi>

<mi>second</mi>

<mi>first</mi>

<mi>second</mi>

<mi>second</mi>

<mi>first</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}</annotation>

</semantics>

</math><img src="./64287c918aeec2d5ac9ab0d0eb46a8b6ef59add4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:145.293ex; height:2.843ex;" alt="{\displaystyle \operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Rational_and_real_numbers">Rational and real numbers</h3></div>

Rational and <a href="Computable_number" title="Computable number">computable real numbers</a> may also be encoded in lambda calculus. Rational numbers may be encoded as a pair of signed numbers. Computable real numbers may be encoded by a limiting process that guarantees that the difference from the real value differs by a number which may be made as small as we need.<a href="#cite_note-8">[6]</a>

<a href="#cite_note-9">[7]</a> The references given describe software that could, in theory, be translated into lambda calculus. Once real numbers are defined, complex numbers are naturally encoded as a pair of real numbers.

The data types and functions described above demonstrate that any data type or calculation may be encoded in lambda calculus. This is the <a href="Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a>.

<div class="mw-heading mw-heading3"><h3 id="Translation_with_other_representations">Translation with other representations</h3></div>

Most real-world languages have support for machine-native integers; the church and unchurch functions convert between nonnegative integers and their corresponding Church numerals. The functions are given here in <a href="Haskell_(programming_language)" class="mw-redirect" title="Haskell (programming language)">Haskell</a>, where the <code>\</code> corresponds to the λ of Lambda calculus. Implementations in other languages are similar.

<div class="mw-highlight mw-highlight-lang-haskell mw-content-ltr" dir="ltr"><pre>type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer

church 0 = \f -> \x -> x

church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer

unchurch cn = cn (+ 1) 0

</pre></div>

<div class="mw-heading mw-heading2"><h2 id="Church_Booleans">Church Booleans</h2></div>

Church Booleans are the Church encoding of the Boolean values true and false. Some programming languages use these as an implementation model for Boolean arithmetic; examples are <a href="Smalltalk" title="Smalltalk">Smalltalk</a> and <a href="Pico_(programming_language)" title="Pico (programming language)">Pico</a>.

Boolean logic may be considered as a choice. The Church encoding of true and false are functions of two parameters:

<ul><li>true chooses the first parameter.</li>

<li>false chooses the second parameter.</li></ul>

The two definitions are known as Church Booleans:

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>false</mi>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}</annotation>

</semantics>

</math><img src="./d39bc19720586d643dd1923cd9e054b1614725f9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.338ex; width:16.555ex; height:5.843ex;" alt="{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}" loading="lazy"></dd></dl>

This definition allows predicates (i.e. functions returning <a href="Truth_value" title="Truth value">logical values</a>) to directly act as if-clauses. A function returning a Boolean, which is then applied to two parameters, returns either the first or the second parameter:

</mrow>

</mrow>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {else-clause} }</annotation>

</semantics>

</math><img src="./40bae3d89eee7730341cd81773860b9971024c18.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:35.987ex; height:2.509ex;" alt="{\displaystyle \operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {else-clause} }" loading="lazy"></dd></dl>

evaluates to then-clause if predicate-x evaluates to true, and to else-clause if predicate-x evaluates to false.

Because true and false choose the first or second parameter they may be combined to provide logic operators. Note that there are multiple possible implementations of not.

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}</annotation>

</semantics>

</math><img src="./5d83df88b47549da4c1e2ec1f43d79fc1d40efa1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -8.505ex; width:51.222ex; height:18.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}" loading="lazy"></dd></dl>

Some examples:

<mtr>

<mtd>

<mi>false</mi>

</mtd>

<mtd>

<mi>false</mi>

<mi>false</mi>

<mi>false</mi>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>false</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}}</annotation>

</semantics>

</math><img src="./a36161f4e76c5ef328c080d27810bb395713209e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -5.671ex; width:134.406ex; height:12.509ex;" alt="{\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading2"><h2 id="Predicates">Predicates</h2></div>

A predicate is a function that returns a Boolean value. The most fundamental predicate is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {IsZero} }">

<mi>IsZero</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {IsZero} }</annotation>

</semantics>

</math><img src="./e5f709697842cf3570b825bca28a60e944eb2d30.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:6.283ex; height:2.176ex;" alt="{\displaystyle \operatorname {IsZero} }" loading="lazy">, which returns <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {true} }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {true} }</annotation>

</semantics>

</math><img src="./a07a936997571bc12ab787780f1297f027b62d17.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.141ex; height:2.009ex;" alt="{\displaystyle \operatorname {true} }" loading="lazy"> if its argument is the Church numeral <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle 0}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle 0}</annotation>

</semantics>

</math><img src="./2aae8864a3c1fec9585261791a809ddec1489950.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.162ex; height:2.176ex;" alt="{\displaystyle 0}" loading="lazy">, and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \operatorname {false} }">

<mi>false</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {false} }</annotation>

</semantics>

</math><img src="./ebe7ab984a6fbcc84fdf934e6ba79acb02e286f3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.47ex; height:2.176ex;" alt="{\displaystyle \operatorname {false} }" loading="lazy"> if its argument is any other Church numeral:

<mi>IsZero</mi>

<mi>false</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} }</annotation>

</semantics>

</math><img src="./9116fab6e6d980cf590c8049c682812bdb020cab.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.247ex; height:2.843ex;" alt="{\displaystyle \operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} }" loading="lazy"></dd></dl>

The following predicate tests whether the first argument is less-than-or-equal-to the second:

<mi>IsZero</mi>

<mi>minus</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)}</annotation>

</semantics>

</math><img src="./8a73f72a8db91a2013be09463c729d0d23f78485.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:36.283ex; height:2.843ex;" alt="{\displaystyle \operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)}" loading="lazy">,</dd></dl>

Because of the identity,

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x=y\equiv (x\leq y\land y\leq x)}</annotation>

</semantics>

</math><img src="./bcaae2c6f4c9d75d3efc656826195c78856263dd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:24.241ex; height:2.843ex;" alt="{\displaystyle x=y\equiv (x\leq y\land y\leq x)}" loading="lazy"></dd></dl>

The test for equality may be implemented as,

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)}</annotation>

</semantics>

</math><img src="./dec6112978637d91f8a46fb1b8d107e62b9fe873.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:43.272ex; height:2.843ex;" alt="{\displaystyle \operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading2"><h2 id="Church_pairs">Church pairs</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">See also: <a href="Cons" title="Cons">Cons</a></div>

Church pairs are the Church encoding of the <a href="Cons" title="Cons">pair</a> (two-tuple) type. The pair is represented as a function that takes a function argument. When given its argument it will apply the argument to the two components of the pair. The definition in <a href="Lambda_calculus" title="Lambda calculus">lambda calculus</a> is,

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>first</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>second</mi>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {pair} &\equiv \lambda xy.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda xy.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda xy.y)\end{aligned}}}</annotation>

</semantics>

</math><img src="./5bbf337725f4f1dda750bd67d5787b540dea166b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -4.005ex; width:23.9ex; height:9.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {pair} &\equiv \lambda xy.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda xy.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda xy.y)\end{aligned}}}" loading="lazy"></dd></dl>

For example,

<mtr>

<mtd>

<mi>first</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ ((\lambda xyz.z\ x\ y)\ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ (\lambda z.z\ a\ b)\\=&\ (\lambda z.z\ a\ b)\ (\lambda xy.x)\\=&\ (\lambda xy.x)\ a\ b\\=&\ a\end{aligned}}}</annotation>

</semantics>

</math><img src="./076fc12e721379e8a1287b12a529c68e19e0ce7f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -8.671ex; width:36.557ex; height:18.509ex;" alt="{\displaystyle {\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ ((\lambda xyz.z\ x\ y)\ a\ b)\\=&\ (\lambda p.p\ (\lambda xy.x))\ (\lambda z.z\ a\ b)\\=&\ (\lambda z.z\ a\ b)\ (\lambda xy.x)\\=&\ (\lambda xy.x)\ a\ b\\=&\ a\end{aligned}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading2"><h2 id="List_encodings">List encodings</h2></div>

An (<a href="Immutable_object" title="Immutable object">immutable</a>) <a href="List_(computing)" class="mw-redirect" title="List (computing)">list</a> is constructed from list nodes. The basic operations on the list are;

<th>Function</th>

<th>Description

</th></tr>

<tr>

<td>Construct an empty list.

</td></tr>

<tr>

<td>isnil</td>

<td>Test if list is empty.

</td></tr>

<tr>

<td>Prepend a given value to a (possibly empty) list.

</td></tr>

<tr>

<td>Get the first element of the list.

</td></tr>

<tr>

<td>Get the rest of the list.

</td></tr></tbody></table>

We give four different representations of lists below:

<ul><li>Build each list node from two pairs (to allow for empty lists).</li>

<li>Build each list node from one pair.</li>

<li>Represent the list using the <a href="Fold_(higher-order_function)" title="Fold (higher-order function)">right fold function</a>.</li>

<li>Represent the list using Scott's encoding that takes cases of match expression as arguments</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Two_pairs_as_a_list_node">Two pairs as a list node</h3></div>

A nonempty list can be implemented by a Church pair;

<ul><li>First contains the head.</li>

<li>Second contains the tail.</li></ul>

However this does not give a representation of the empty list, because there is no "null" pointer. To represent null, the pair may be wrapped in another pair, giving three values:

<ul><li>First - the null pointer (empty list).</li>

<li>Second.First contains the head.</li>

<li>Second.Second contains the tail.</li></ul>

Using this idea the basic list operations can be defined like this:<a href="#cite_note-10">[8]</a>

<th>Expression</th>

<th>Description

</th></tr>

<tr>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true} }</annotation>

</semantics>

</math><img src="./7886719e74c6ac406b5aab21fc86cae89532790c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:20.69ex; height:2.509ex;" alt="{\displaystyle \operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true} }" loading="lazy">

</td>

<td>The first element of the pair is true meaning the list is null.

</td></tr>

<tr>

<mi>isnil</mi>

<mi>first</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {isnil} \equiv \operatorname {first} }</annotation>

</semantics>

</math><img src="./370060d161fe0ea133973730c1582092afd57253.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:11.339ex; height:2.176ex;" alt="{\displaystyle \operatorname {isnil} \equiv \operatorname {first} }" loading="lazy">

</td>

<td>Retrieve the null (or empty list) indicator.

</td></tr>

<tr>

<mi>false</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)}</annotation>

</semantics>

</math><img src="./f8e6b19a9f0edc1836c728f7e230b3ff57d83204.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.266ex; height:2.843ex;" alt="{\displaystyle \operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)}" loading="lazy">

</td>

<td>Create a list node, which is not null, and give it a head h and a tail t.

</td></tr>

<tr>

<mi>first</mi>

<mi>second</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)}</annotation>

</semantics>

</math><img src="./7b73603a34e398c6adef333c909c856fdff31e48.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:26.428ex; height:2.843ex;" alt="{\displaystyle \operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)}" loading="lazy">

</td>

<td>second.first is the head.

</td></tr>

<tr>

<mi>second</mi>

<mi>second</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)}</annotation>

</semantics>

</math><img src="./2870dc90bc32e4962ecd92a8175f8ed1530d76f9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.646ex; height:2.843ex;" alt="{\displaystyle \operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)}" loading="lazy">

</td>

<td>second.second is the tail.

</td></tr></tbody></table>

In a nil node second is never accessed, provided that head and tail are only applied to nonempty lists.

Alternatively, define<a href="#cite_note-11">[9]</a>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mrow>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>isnil</mi>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {\{-first-\}} \equiv \lambda l.\ l\ (\lambda htd.\ h)\ \operatorname {nil} \\\operatorname {tail} &\equiv \operatorname {\{-second-\}} \equiv \lambda l.\ l\ (\lambda htd.\ t)\ \operatorname {nil} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda htd.\operatorname {false} )\operatorname {true} \\\end{aligned}}}</annotation>

</semantics>

</math><img src="./fe75a96c29474c8174cc0a3c3dd8f06808e8a37b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.005ex; width:39.835ex; height:15.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {\{-first-\}} \equiv \lambda l.\ l\ (\lambda htd.\ h)\ \operatorname {nil} \\\operatorname {tail} &\equiv \operatorname {\{-second-\}} \equiv \lambda l.\ l\ (\lambda htd.\ t)\ \operatorname {nil} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda htd.\operatorname {false} )\operatorname {true} \\\end{aligned}}}" loading="lazy"></dd></dl>

where the definitions like the last one follow the general pattern of the safe use of a list, where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle h}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle h}</annotation>

</semantics>

</math><img src="./b26be3e694314bc90c3215047e4a2010c6ee184a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.339ex; height:2.176ex;" alt="{\displaystyle h}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle t}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle t}</annotation>

</semantics>

</math><img src="./65658b7b223af9e1acc877d848888ecdb4466560.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.84ex; height:2.009ex;" alt="{\displaystyle t}" loading="lazy"> refer to the list's head and tail:

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mrow>

</mrow>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {process-list} &\equiv \lambda l.l\ (\lambda htd.\langle \operatorname {head-and-tail-clause} \rangle )\ \langle \operatorname {nil-clause} \rangle \\\end{aligned}}}</annotation>

</semantics>

</math><img src="./5a52888d55fd3dfc1b20daa3c9f74daacbd3aa8b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:60.89ex; height:2.843ex;" alt="{\displaystyle {\begin{aligned}\operatorname {process-list} &\equiv \lambda l.l\ (\lambda htd.\langle \operatorname {head-and-tail-clause} \rangle )\ \langle \operatorname {nil-clause} \rangle \\\end{aligned}}}" loading="lazy"></dd></dl>

Other operations for one pair as a list node

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>rfold</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>length</mi>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {fold} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda al.\ l\ (\lambda htd.\ r\ (f\ a\ h)\ t)\ a)\\\operatorname {rfold} &\equiv \lambda fa.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda htd.\ f\ (r\ t)\ h)\ a)\\\operatorname {length} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {succ} \ a)\ \operatorname {zero} \end{aligned}}}</annotation>

</semantics>

</math><img src="./a5d3697224e9bc0922583963bba2349477d82a8f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -4.005ex; width:48.793ex; height:9.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {fold} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda al.\ l\ (\lambda htd.\ r\ (f\ a\ h)\ t)\ a)\\\operatorname {rfold} &\equiv \lambda fa.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda htd.\ f\ (r\ t)\ h)\ a)\\\operatorname {length} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {succ} \ a)\ \operatorname {zero} \end{aligned}}}" loading="lazy"></dd></dl>

<hr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>rfold</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>filter</mi>

</mtd>

<mtd>

<mi>rfold</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>reverse</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>concat</mi>

</mtd>

<mtd>

<mi>rfold</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>concat</mi>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {map} &\equiv \lambda f.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ (f\ h)\ a)\ \operatorname {nil} \\\operatorname {filter} &\equiv \lambda p.\ \operatorname {rfold} \ (\lambda ah.\ p\ h\ (\operatorname {cons} \ h\ a)\ a)\ \operatorname {nil} \\\operatorname {reverse} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ \operatorname {nil} \\\operatorname {concat} &\equiv \lambda lg.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ g\ l\\\operatorname {conj} &\equiv \lambda lv.\ \operatorname {concat} \ l\ (\operatorname {cons} \ v\ \operatorname {nil} )\end{aligned}}}</annotation>

</semantics>

</math><img src="./48445e30689e6ad1fc888f123ca9519814029ff7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -7.171ex; width:47.846ex; height:15.509ex;" alt="{\displaystyle {\begin{aligned}\operatorname {map} &\equiv \lambda f.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ (f\ h)\ a)\ \operatorname {nil} \\\operatorname {filter} &\equiv \lambda p.\ \operatorname {rfold} \ (\lambda ah.\ p\ h\ (\operatorname {cons} \ h\ a)\ a)\ \operatorname {nil} \\\operatorname {reverse} &\equiv \operatorname {fold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ \operatorname {nil} \\\operatorname {concat} &\equiv \lambda lg.\ \operatorname {rfold} \ (\lambda ah.\ \operatorname {cons} \ h\ a)\ g\ l\\\operatorname {conj} &\equiv \lambda lv.\ \operatorname {concat} \ l\ (\operatorname {cons} \ v\ \operatorname {nil} )\end{aligned}}}" loading="lazy"></dd></dl>

<hr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>IsZero</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

<mi>IsZero</mi>

<mi>second</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mi>IsZero</mi>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>IsZero</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

<mi>IsZero</mi>

<mi>second</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mi>IsZero</mi>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {drop} &\equiv \lambda n.\ n\ \operatorname {tail} \\&\equiv \operatorname {Y} \ (\lambda r.\lambda nl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ l\ (r\ (\operatorname {pred} \ n)\ t))\ \operatorname {nil} )\\\operatorname {drop-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ (\operatorname {cons} \ h\ l_{a}))\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ \operatorname {nil} )\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l\ )\\\operatorname {drop-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (r\ t)\ l)\ \operatorname {nil} )\\\operatorname {take} &\equiv \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ h\ (r\ (\operatorname {pred} \ n)\ t)))\ \operatorname {nil} )\\\operatorname {take-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ l_{a})\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ l_{r})\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l)\\\operatorname {take-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (\operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\ \operatorname {nil} )\end{aligned}}}</annotation>

</semantics>

</math><img src="./a97120eadcde48b74d771ab88846baae9360417f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -29.005ex; width:74.422ex; height:59.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {drop} &\equiv \lambda n.\ n\ \operatorname {tail} \\&\equiv \operatorname {Y} \ (\lambda r.\lambda nl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ l\ (r\ (\operatorname {pred} \ n)\ t))\ \operatorname {nil} )\\\operatorname {drop-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ (\operatorname {cons} \ h\ l_{a}))\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ \operatorname {nil} )\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l\ )\\\operatorname {drop-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (r\ t)\ l)\ \operatorname {nil} )\\\operatorname {take} &\equiv \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ h\ (r\ (\operatorname {pred} \ n)\ t)))\ \operatorname {nil} )\\\operatorname {take-last} &\equiv \lambda nl.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \ \ \ \ \operatorname {Y} \ (\lambda rl_{r}.\ l_{r}\ (\lambda htd.\\&\ \ \ \ \ \ \ \ \ \ \ \ r\ t\ (\lambda n_{a}l_{a}.\ \operatorname {IsZero} \ n_{a}\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ l_{a})\\&\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ n_{a})\ l_{r})\ ))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\ )\\&\ \ \ \ \ \ \ \ \ l)\\\operatorname {take-while} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rl.\ l\ (\lambda htd.\ p\ h\ (\operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\ \operatorname {nil} )\end{aligned}}}" loading="lazy"></dd></dl>

<hr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

<mi>concat</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

<mi>concat</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

<mi>concat</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mrow>

</mtd>

<mtd>

<mi>IsZero</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>range</mi>

</mtd>

<mtd>

<mi>IsZero</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>repeat</mi>

</mtd>

<mtd>

<mi>IsZero</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {all} &\equiv \operatorname {Y} \ (\lambda rpl.\ l\ (\lambda htd.\ p\ h\ (r\ p\ t)\ \operatorname {false} )\ \operatorname {true} )\\\operatorname {any} &\equiv \operatorname {Y} \ (\lambda rpl.\ l\ (\lambda htd.\ p\ h\ \operatorname {true} \ (r\ p\ t))\ \operatorname {false} )\\\operatorname {element-at} &\equiv \lambda nl.\ \operatorname {head} \ (\operatorname {drop} \ n\ l)\\\operatorname {insert-at} &\equiv \lambda nvl.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {cons} \ v\ (\operatorname {drop} \ n\ l))\\\operatorname {remove-at} &\equiv \lambda nl.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {drop} \ (\operatorname {succ} \ n)\ l)\\\operatorname {replace-at} &\equiv \lambda nvl.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {cons} \ v\ (\operatorname {drop} \ (\operatorname {succ} \ n)\ l))\\\operatorname {index-of} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ p\ h\ n\ (r\ (\operatorname {succ} \ n)\ t))\ \operatorname {zero} )\ \operatorname {one} \\\operatorname {last-index-of} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ (\lambda i.\ \operatorname {IsZero} \ i\ (p\ h\ n\ \operatorname {zero} )\ i)\ (r\ (\operatorname {succ} \ n)\ t))\ \operatorname {zero} )\ \operatorname {one} \\\operatorname {range} &\equiv \lambda fz.\ \operatorname {Y} \ (\lambda rsn.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ (s\ f\ z)\ (r\ (\operatorname {succ} \ s)\ (\operatorname {pred} \ n))))\ \operatorname {zero} \\\operatorname {repeat} &\equiv \lambda v.\ \operatorname {Y} \ (\lambda rn.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ v\ (r\ (\operatorname {pred} \ n))))\\\operatorname {zip} &\equiv Y\ (\lambda rl_{1}l_{2}.\ l_{1}\ (\lambda h_{1}t_{1}d_{1}.\ l_{2}\ (\lambda h_{2}t_{2}d_{2}.\ \operatorname {cons} \ (\operatorname {pair} \ h_{1}\ h_{2})\ (r\ t_{1}\ t_{2}))\ \operatorname {nil} )\ \operatorname {nil} )\\\end{aligned}}}</annotation>

</semantics>

</math><img src="./3bc8625539fc8a72649f0f02cf759af8e22fc53a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -16.505ex; width:92.561ex; height:34.176ex;" alt="{\displaystyle {\begin{aligned}\operatorname {all} &\equiv \operatorname {Y} \ (\lambda rpl.\ l\ (\lambda htd.\ p\ h\ (r\ p\ t)\ \operatorname {false} )\ \operatorname {true} )\\\operatorname {any} &\equiv \operatorname {Y} \ (\lambda rpl.\ l\ (\lambda htd.\ p\ h\ \operatorname {true} \ (r\ p\ t))\ \operatorname {false} )\\\operatorname {element-at} &\equiv \lambda nl.\ \operatorname {head} \ (\operatorname {drop} \ n\ l)\\\operatorname {insert-at} &\equiv \lambda nvl.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {cons} \ v\ (\operatorname {drop} \ n\ l))\\\operatorname {remove-at} &\equiv \lambda nl.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {drop} \ (\operatorname {succ} \ n)\ l)\\\operatorname {replace-at} &\equiv \lambda nvl.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {cons} \ v\ (\operatorname {drop} \ (\operatorname {succ} \ n)\ l))\\\operatorname {index-of} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ p\ h\ n\ (r\ (\operatorname {succ} \ n)\ t))\ \operatorname {zero} )\ \operatorname {one} \\\operatorname {last-index-of} &\equiv \lambda p.\ \operatorname {Y} \ (\lambda rnl.\ l\ (\lambda htd.\ (\lambda i.\ \operatorname {IsZero} \ i\ (p\ h\ n\ \operatorname {zero} )\ i)\ (r\ (\operatorname {succ} \ n)\ t))\ \operatorname {zero} )\ \operatorname {one} \\\operatorname {range} &\equiv \lambda fz.\ \operatorname {Y} \ (\lambda rsn.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ (s\ f\ z)\ (r\ (\operatorname {succ} \ s)\ (\operatorname {pred} \ n))))\ \operatorname {zero} \\\operatorname {repeat} &\equiv \lambda v.\ \operatorname {Y} \ (\lambda rn.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ v\ (r\ (\operatorname {pred} \ n))))\\\operatorname {zip} &\equiv Y\ (\lambda rl_{1}l_{2}.\ l_{1}\ (\lambda h_{1}t_{1}d_{1}.\ l_{2}\ (\lambda h_{2}t_{2}d_{2}.\ \operatorname {cons} \ (\operatorname {pair} \ h_{1}\ h_{2})\ (r\ t_{1}\ t_{2}))\ \operatorname {nil} )\ \operatorname {nil} )\\\end{aligned}}}" loading="lazy"></dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Represent_the_list_using_right_fold">Represent the list using right fold</h3></div>

As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its <a href="Fold_(higher-order_function)" title="Fold (higher-order function)">right fold function</a>. For example, a list of three elements x, y and z can be encoded by a higher-order function that when applied to a combinator c and a value n returns c x (c y (c z n)). Equivalently, it is an application of the chain of functional compositions of partial applications, (c x <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \circ }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \circ }</annotation>

</semantics>

</math><img src="./99add39d2b681e2de7ff62422c32704a05c7ec31.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.125ex; margin-bottom: -0.297ex; width:1.162ex; height:1.509ex;" alt="{\displaystyle \circ }" loading="lazy"> c y <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \circ }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \circ }</annotation>

</semantics>

</math><img src="./99add39d2b681e2de7ff62422c32704a05c7ec31.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.125ex; margin-bottom: -0.297ex; width:1.162ex; height:1.509ex;" alt="{\displaystyle \circ }" loading="lazy"> c z) n.

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>singleton</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>append</mi>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>isnil</mi>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

<mi>nonempty</mi>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

<mi>false</mi>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

<mtr>

<mtd>

</mtd>

<mtd>

</mtd>

</mtr>

</mtable>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {singleton} &\equiv \lambda h.\lambda c.\lambda n.c\ h\ n\\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {append} &\equiv \lambda l.\lambda t.\lambda c.\lambda n.l\ c\ (t\ c\ n)\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda r.\operatorname {false} )\ \operatorname {true} \\\operatorname {nonempty} &\equiv \lambda l.l\ (\lambda h.\lambda r.true)\ \operatorname {false} \\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda r.h)\ \operatorname {false} \\\operatorname {map} &\equiv \lambda f.\lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.c\ (f\ h)\ r)\ n\\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.\lambda g.g\ h\ (r\ c))\ (\lambda c.n)\ (\lambda h.\lambda t.t)\end{aligned}}}</annotation>

</semantics>

</math><img src="./3aecfb4e2c2edc62c791beea684a5a671c166258.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -13.338ex; width:63.436ex; height:27.843ex;" alt="{\displaystyle {\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {singleton} &\equiv \lambda h.\lambda c.\lambda n.c\ h\ n\\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {append} &\equiv \lambda l.\lambda t.\lambda c.\lambda n.l\ c\ (t\ c\ n)\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda r.\operatorname {false} )\ \operatorname {true} \\\operatorname {nonempty} &\equiv \lambda l.l\ (\lambda h.\lambda r.true)\ \operatorname {false} \\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda r.h)\ \operatorname {false} \\\operatorname {map} &\equiv \lambda f.\lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.c\ (f\ h)\ r)\ n\\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.\lambda g.g\ h\ (r\ c))\ (\lambda c.n)\ (\lambda h.\lambda t.t)\end{aligned}}}" loading="lazy"></dd></dl>

This list representation can be given type in <a href="System_F" title="System F">System F</a>.

The evident correspondence to Church numerals is non-coincidental, as that can be seen as a unary encoding, with natural numbers represented by lists of unit (i.e. non-important) values, e.g. [() () ()], with the list's length serving as the representation of the natural number. Right folding over such lists uses functions which necessarily ignore the element's value, and is equivalent to the chained functional composition, i.e. (c () <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \circ }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \circ }</annotation>

</semantics>

</math><img src="./99add39d2b681e2de7ff62422c32704a05c7ec31.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.125ex; margin-bottom: -0.297ex; width:1.162ex; height:1.509ex;" alt="{\displaystyle \circ }" loading="lazy"> c () <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \circ }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \circ }</annotation>

</semantics>

</math><img src="./99add39d2b681e2de7ff62422c32704a05c7ec31.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.125ex; margin-bottom: -0.297ex; width:1.162ex; height:1.509ex;" alt="{\displaystyle \circ }" loading="lazy"> c ()) n = (f <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \circ }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \circ }</annotation>

</semantics>

</math><img src="./99add39d2b681e2de7ff62422c32704a05c7ec31.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.125ex; margin-bottom: -0.297ex; width:1.162ex; height:1.509ex;" alt="{\displaystyle \circ }" loading="lazy"> f <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \circ }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \circ }</annotation>

</semantics>

</math><img src="./99add39d2b681e2de7ff62422c32704a05c7ec31.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.125ex; margin-bottom: -0.297ex; width:1.162ex; height:1.509ex;" alt="{\displaystyle \circ }" loading="lazy"> f) n, as is used in Church numerals.

<div class="mw-heading mw-heading3"><h3 id="Represent_the_list_using_Scott_encoding">Represent the list using Scott encoding</h3></div>

An alternative representation is Scott encoding, which uses the idea of <a href="Continuation" title="Continuation">continuations</a> and can lead to simpler code.<a href="#cite_note-12">[10]</a> (see also <a href="Mogensen%E2%80%93Scott_encoding" title="Mogensen–Scott encoding">Mogensen–Scott encoding</a>).

In this approach, we use the fact that lists can be observed using <a href="Pattern_matching" title="Pattern matching">pattern matching</a> expression. For example, using <a href="Scala_(programming_language)" title="Scala (programming language)">Scala</a> notation, if <code>list</code> denotes a value of type <code>List</code> with empty list <code>Nil</code> and constructor <code>Cons(h, t)</code> we can inspect the list and compute <code>nilCode</code> in case the list is empty and <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">consCode(h, t)</code> when the list is not empty:

<div class="mw-highlight mw-highlight-lang-scala mw-content-ltr" dir="ltr"><pre>list match {

case Nil => nilCode

case Cons(h, t) => consCode(h,t)

}

</pre></div>

The <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">list</code> is given by how it acts upon <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">nilCode</code> and <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">consCode</code>. We therefore define a list as a function that accepts such <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">nilCode</code> and <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">consCode</code> as arguments, so that instead of the above pattern match we may simply write:

<mi>nilCode</mi>

<mi>consCode</mi>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode} }</annotation>

</semantics>

</math><img src="./2fed5c2170dc6524f47dfb1332f4b1e9eef58e33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:23.145ex; height:2.176ex;" alt="{\displaystyle \operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode} }" loading="lazy"></dd></dl>

Let us denote by <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">n</code> the parameter corresponding to <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">nilCode</code> and by <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">c</code> the parameter corresponding to <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">consCode</code>.

The empty list is the one that returns the nil argument:

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {nil} \equiv \lambda n.\lambda c.\ n}</annotation>

</semantics>

</math><img src="./061977d5c1ff321964e23272b8f6975482432a9b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:14.84ex; height:2.176ex;" alt="{\displaystyle \operatorname {nil} \equiv \lambda n.\lambda c.\ n}" loading="lazy"></dd></dl>

The non-empty list with head <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">h</code> and tail <code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">t</code> is given by

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \operatorname {cons} \ h\ t\ \ \equiv \ \ \lambda n.\lambda c.\ c\ h\ t}</annotation>

</semantics>

</math><img src="./029fdcc34b5e31c2b40ed4e96261d22394e4e823.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:25.659ex; height:2.176ex;" alt="{\displaystyle \operatorname {cons} \ h\ t\ \ \equiv \ \ \lambda n.\lambda c.\ c\ h\ t}" loading="lazy"></dd></dl>

More generally, an <a href="Algebraic_data_type" title="Algebraic data type">algebraic data type</a> with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle m}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m}</annotation>

</semantics>

</math><img src="./0a07d98bb302f3856cbabc47b2b9016692e3f7bc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.04ex; height:1.676ex;" alt="{\displaystyle m}" loading="lazy"> alternatives becomes a function with <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle m}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle m}</annotation>

</semantics>

</math><img src="./0a07d98bb302f3856cbabc47b2b9016692e3f7bc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.04ex; height:1.676ex;" alt="{\displaystyle m}" loading="lazy"> parameters. When the <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle i}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle i}</annotation>

</semantics>

</math><img src="./add78d8608ad86e54951b8c8bd6c8d8416533d20.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.802ex; height:2.176ex;" alt="{\displaystyle i}" loading="lazy">th constructor has <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n_{i}}</annotation>

</semantics>

</math><img src="./57f87f905ba5a4d8c691ccaecd65fc47bd007ba4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.194ex; height:2.009ex;" alt="{\displaystyle n_{i}}" loading="lazy"> arguments, the corresponding parameter of the encoding takes <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle n_{i}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle n_{i}}</annotation>

</semantics>

</math><img src="./57f87f905ba5a4d8c691ccaecd65fc47bd007ba4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.194ex; height:2.009ex;" alt="{\displaystyle n_{i}}" loading="lazy"> arguments as well.

Scott encoding can be done in untyped lambda calculus, whereas its use with types requires a type system with recursion and type polymorphism. A list with element type E in this representation that is used to compute values of type C would have the following recursive type definition, where '=>' denotes <a href="Function_type" title="Function type">function type</a>:

<div class="mw-highlight mw-highlight-lang-scala mw-content-ltr" dir="ltr"><pre>type List =

C => // nil argument

(E => List => C) => // cons argument

C // result of pattern matching

</pre></div>

A list that can be used to compute arbitrary types would have a type that quantifies over <code>C</code>. A list generic in <code>E</code> would also take <code>E</code> as the type argument.

<ul><li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li>

<li><a href="System_F" title="System F">System F</a> for Church numerals in a typed calculus</li>

<li><a href="Mogensen%E2%80%93Scott_encoding" title="Mogensen–Scott encoding">Mogensen–Scott encoding</a></li>

<li><a href="Ordinal_number#Von_Neumann_definition_of_ordinals" title="Ordinal number">Von Neumann definition of ordinals</a> — another way to encode natural numbers: as sets</li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFTrancón_y_WidemannParnas2008" class="citation conference cs1">Trancón y Widemann, Baltasar; Parnas, David Lorge (2008). "Tabular Expressions and Total Functional Programming". In Olaf Chitil; Zoltán Horváth; Viktória Zsók (eds.). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=E1zuY1Q6sOsC&pg=PA228">Implementation and Application of Functional Languages</a>. 19th International Workshop, IFL 2007, Freiburg, Germany, September 27–29, 2007 Revised Selected Papers. Lecture Notes in Computer Science. Vol. 5083. pp. 228–229. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-540-85373-2_13">10.1007/978-3-540-85373-2_13</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-85372-5</bdi>.</cite>

</li>

<li id="cite_note-2"><a href="#cite_ref-2">^</a> <cite id="CITEREFJansenKoopmanPlasmeijer2006" class="citation book cs1">Jansen, Jan Martin; Koopman, Pieter W. M.; Plasmeijer, Marinus J. (2006). "Efficient interpretation by transforming data types and patterns to functions". In Nilsson, Henrik (ed.). Trends in functional programming. Volume 7. Bristol: Intellect. pp. 73–90. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.73.9841">10.1.1.73.9841</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-84150-188-8</bdi>.</cite>

</li>

<li id="cite_note-3"><a href="#cite_ref-3">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://okmij.org/ftp/Computation/lambda-calc.html#predecessor">"Predecessor and lists are not representable in simply typed lambda calculus"</a>. Lambda Calculus and Lambda Calculators. okmij.org.</cite>

</li>

<cite id="CITEREFAllison" class="citation web cs1">Allison, Lloyd. <a rel="nofollow" class="external text" href="http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/const-int/">"Lambda Calculus Integers"</a>.</cite>

</li>

<cite id="CITEREFBauer" class="citation web cs1">Bauer, Andrej. <a rel="nofollow" class="external text" href="https://cs.stackexchange.com/q/2272">"Andrej's answer to a question; "Representing negative and complex numbers using lambda calculus""</a>.</cite>

</li>

<cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://wiki.haskell.org/Exact_real_arithmetic">"Exact real arithmetic"</a>. Haskell. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20150326164041/https://wiki.haskell.org/Exact_real_arithmetic">Archived</a> from the original on 2015-03-26.</cite>

</li>

<cite id="CITEREFBauer2022" class="citation web cs1">Bauer, Andrej (26 September 2022). <a rel="nofollow" class="external text" href="https://github.com/andrejbauer/marshall">"Real number computational software"</a>. <a href="GitHub" title="GitHub">GitHub</a>.</cite>

</li>

<li id="cite_note-10"><a href="#cite_ref-10">^</a> <cite id="CITEREFPierce2002" class="citation book cs1"><a href="Benjamin_C._Pierce" title="Benjamin C. Pierce">Pierce, Benjamin C.</a> (2002). <a href="Types_and_Programming_Languages" title="Types and Programming Languages">Types and Programming Languages</a>. <a href="MIT_Press" title="MIT Press">MIT Press</a>. p. 500. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-262-16209-8</bdi>.</cite>

</li>

<li id="cite_note-11"><a href="#cite_ref-11">^</a> <cite id="CITEREFTromp2007" class="citation book cs1">Tromp, John (2007). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=flPICgAAQBAJ&pg=PP1">"14. Binary Lambda Calculus and Combinatory Logic"</a>. In Calude, Cristian S (ed.). Randomness And Complexity, From Leibniz To Chaitin. World Scientific. pp. 237–262. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-981-4474-39-9</bdi>.</cite> As PDF: <cite id="CITEREFTromp2014" class="citation web cs1">Tromp, John (14 May 2014). <a rel="nofollow" class="external text" href="https://tromp.github.io/cl/LC.pdf">"Binary Lambda Calculus and Combinatory Logic"</a> (PDF). Retrieved 2017-11-24.</cite>

</li>

<li id="cite_note-12"><a href="#cite_ref-12">^</a> <cite id="CITEREFJansen2013" class="citation book cs1">Jansen, Jan Martin (2013). "Programming in the λ-Calculus: From Church to Scott and Back". In Achten, Peter; Koopman, Pieter W. M. (eds.). The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday. Lecture Notes in Computer Science. Vol. 8106. Springer. pp. 168–180. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-40355-2_12">10.1007/978-3-642-40355-2_12</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-642-40354-5</bdi>.</cite>

</li>

</ol></div>

<ul><li><cite id="CITEREFStump2009" class="citation journal cs1">Stump, A. (2009). <a rel="nofollow" class="external text" href="http://www.cs.uiowa.edu/~astump/papers/archon.pdf">"Directly reflective meta-programming"</a> (PDF). High-Order Symb Comput. 22 (2): 115–144. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.489.5018">10.1.1.489.5018</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10990-007-9022-0">10.1007/s10990-007-9022-0</a>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:16124152">16124152</a>.</cite></li>

<li><cite id="CITEREFCartwright" class="citation web cs1">Cartwright, Robert. <a rel="nofollow" class="external text" href="http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf">"Church numerals and booleans explained"</a> (PDF). Comp 311 — Review 2. <a href="Rice_University" title="Rice University">Rice University</a>.</cite></li>

<li><cite id="CITEREFKemp2007" class="citation thesis cs1">Kemp, Colin (2007). <a rel="nofollow" class="external text" href="https://espace.library.uq.edu.au/view/UQ:171001">"§2.4.1 Church Naturals, §2.4.2 Church Booleans, Ch. 5 Derivation techniques for TFP"</a>. Theoretical Foundations for Practical 'Totally Functional Programming' (PhD). School of Information Technology and Electrical Engineering, The University of Queensland. pp. 14–17, 93–145. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.149.3505">10.1.1.149.3505</a>.</cite> All about Church and other similar encodings, including how to derive them and operations on them, from first principles</li>

<li><a rel="nofollow" class="external text" href="http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/const-int/">Some interactive examples of Church numerals</a></li>

<li><a rel="nofollow" class="external text" href="http://blog.klipse.tech/lambda/2016/07/24/lambda-calculus-2.html">Lambda Calculus Live Tutorial: Boolean Algebra</a></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Mathematical_logic344" style="padding:3px"><table class="nowraplinks mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Mathematical_logic344" style="font-size:114%;margin:0 4em"><a href="Mathematical_logic" title="Mathematical logic">Mathematical logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">General</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Axiom" title="Axiom">Axiom</a>

<li><a href="Cardinality" title="Cardinality">Cardinality</a></li>

<li><a href="First-order_logic" title="First-order logic">First-order logic</a></li>

<li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>

<li><a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics</a></li>

<li><a href="Foundations_of_mathematics" title="Foundations of mathematics">Foundations of mathematics</a></li>

<li><a href="Information_theory" title="Information theory">Information theory</a></li>

<li><a href="Lemma_(mathematics)" title="Lemma (mathematics)">Lemma</a></li>

<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>

<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a></li>

<li><a href="Theorem" title="Theorem">Theorem</a></li>

<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a></li>

<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Theorems (list)  and <a href="Paradoxes_of_set_theory" title="Paradoxes of set theory">paradoxes</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="G%C3%B6del's_completeness_theorem" title="Gödel's completeness theorem">Gödel's completeness</a> and <a href="G%C3%B6del's_incompleteness_theorems" title="Gödel's incompleteness theorems">incompleteness theorems</a></li>

<li><a href="Tarski's_undefinability_theorem" title="Tarski's undefinability theorem">Tarski's undefinability</a></li>

<li><a href="Banach%E2%80%93Tarski_paradox" title="Banach–Tarski paradox">Banach–Tarski paradox</a></li>

<li>Cantor's <a href="Cantor's_theorem" title="Cantor's theorem">theorem,</a> <a href="Cantor's_paradox" title="Cantor's paradox">paradox</a> and <a href="Cantor's_diagonal_argument" title="Cantor's diagonal argument">diagonal argument</a></li>

<li><a href="Compactness_theorem" title="Compactness theorem">Compactness</a></li>

<li><a href="Halting_problem" title="Halting problem">Halting problem</a></li>

<li><a href="Lindstr%C3%B6m's_theorem" title="Lindström's theorem">Lindström's</a></li>

<li><a href="L%C3%B6wenheim%E2%80%93Skolem_theorem" title="Löwenheim–Skolem theorem">Löwenheim–Skolem</a></li>

<li><a href="Russell's_paradox" title="Russell's paradox">Russell's paradox</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Logic" title="Logic">Logics</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th id="Traditional95" scope="row" class="navbox-group" style="width:1%"><a href="Term_logic" title="Term logic">Traditional</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Classical_logic" title="Classical logic">Classical logic</a></li>

<li><a href="Logical_truth" title="Logical truth">Logical truth</a></li>

<li><a href="Tautology_(logic)" title="Tautology (logic)">Tautology</a></li>

<li><a href="Proposition" title="Proposition">Proposition</a></li>

<li><a href="Inference" title="Inference">Inference</a></li>

<li><a href="Logical_equivalence" title="Logical equivalence">Logical equivalence</a></li>

<li><a href="Consistency" title="Consistency">Consistency</a>

<ul><li><a href="Equiconsistency" title="Equiconsistency">Equiconsistency</a></li></ul></li>

<li><a href="Argument" title="Argument">Argument</a></li>

<li><a href="Soundness" title="Soundness">Soundness</a></li>

<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li>

<li><a href="Syllogism" title="Syllogism">Syllogism</a></li>

<li><a href="Square_of_opposition" title="Square of opposition">Square of opposition</a></li>

<li><a href="Venn_diagram" title="Venn diagram">Venn diagram</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Boolean_algebra" title="Boolean algebra">Boolean algebra</a></li>

<li><a href="Boolean_function" title="Boolean function">Boolean functions</a></li>

<li><a href="Logical_connective" title="Logical connective">Logical connectives</a></li>

<li><a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional calculus</a></li>

<li><a href="Propositional_formula" title="Propositional formula">Propositional formula</a></li>

<li><a href="Truth_table" title="Truth table">Truth tables</a></li>

<li><a href="Many-valued_logic" title="Many-valued logic">Many-valued logic</a>

<li><a href="Finite-valued_logic" title="Finite-valued logic">finite</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Predicate_logic" class="mw-redirect" title="Predicate logic">Predicate</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="First-order_logic" title="First-order logic">First-order</a>

<li><a href="Second-order_logic" title="Second-order logic">Second-order</a>

<ul><li><a href="Monadic_second-order_logic" title="Monadic second-order logic">Monadic</a></li></ul></li>

<li><a href="Higher-order_logic" title="Higher-order logic">Higher-order</a></li>

<li><a href="Fixed-point_logic" title="Fixed-point logic">Fixed-point</a></li>

<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifiers</a></li>

<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a></li>

<li><a href="Monadic_predicate_calculus" title="Monadic predicate calculus">Monadic predicate calculus</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Set_theory" title="Set theory">Set theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Hereditary_set" title="Hereditary set">hereditary</a></li></ul></li>

<li><a href="Class_(set_theory)" title="Class (set theory)">Class</a></li>

<li>(<a href="Urelement" title="Urelement">Ur-</a>)<a href="Element_(mathematics)" title="Element (mathematics)">Element</a></li>

<li><a href="Ordinal_number" title="Ordinal number">Ordinal number</a></li>

<li><a href="Extensionality" title="Extensionality">Extensionality</a></li>

<li><a href="Forcing_(mathematics)" title="Forcing (mathematics)">Forcing</a></li>

<li><a href="Relation_(mathematics)" title="Relation (mathematics)">Relation</a>

<ul><li><a href="Equivalence_relation" title="Equivalence relation">equivalence</a></li>

<li><a href="Partition_of_a_set" title="Partition of a set">partition</a></li></ul></li>

<li>Set operations:

<ul><li><a href="Intersection_(set_theory)" title="Intersection (set theory)">intersection</a></li>

<li><a href="Union_(set_theory)" title="Union (set theory)">union</a></li>

<li><a href="Complement_(set_theory)" title="Complement (set theory)">complement</a></li>

<li><a href="Cartesian_product" title="Cartesian product">Cartesian product</a></li>

<li><a href="Power_set" title="Power set">power set</a></li>

<li><a href="List_of_set_identities_and_relations" title="List of set identities and relations">identities</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Types of <a href="Set_(mathematics)" title="Set (mathematics)">sets</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Countable_set" title="Countable set">Countable</a></li>

<li><a href="Uncountable_set" title="Uncountable set">Uncountable</a></li>

<li><a href="Empty_set" title="Empty set">Empty</a></li>

<li><a href="Inhabited_set" title="Inhabited set">Inhabited</a></li>

<li><a href="Singleton_(mathematics)" title="Singleton (mathematics)">Singleton</a></li>

<li><a href="Finite_set" title="Finite set">Finite</a></li>

<li><a href="Infinite_set" title="Infinite set">Infinite</a></li>

<li><a href="Transitive_set" title="Transitive set">Transitive</a></li>

<li><a href="Ultrafilter_(set_theory)" class="mw-redirect" title="Ultrafilter (set theory)">Ultrafilter</a></li>

<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive</a></li>

<li><a href="Fuzzy_set" title="Fuzzy set">Fuzzy</a></li>

<li><a href="Universal_set" title="Universal set">Universal</a></li>

<li><a href="Universe_(mathematics)" title="Universe (mathematics)">Universe</a>

<ul><li><a href="Constructible_universe" title="Constructible universe">constructible</a></li>

<li><a href="Grothendieck_universe" title="Grothendieck universe">Grothendieck</a></li>

<li><a href="Von_Neumann_universe" title="Von Neumann universe">Von Neumann</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Map_(mathematics)" title="Map (mathematics)">Maps</a> and <a href="Cardinality" title="Cardinality">cardinality</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Function_(mathematics)" title="Function (mathematics)">Function</a>/<a href="Map_(mathematics)" title="Map (mathematics)">Map</a>

<ul><li><a href="Domain_of_a_function" title="Domain of a function">domain</a></li>

<li><a href="Codomain" title="Codomain">codomain</a></li>

<li><a href="Image_(mathematics)" title="Image (mathematics)">image</a></li></ul></li>

<li><a href="Injective_function" title="Injective function">In</a>/<a href="Surjective_function" title="Surjective function">Sur</a>/<a href="Bijection" title="Bijection">Bi</a>-jection</li>

<li><a href="Schr%C3%B6der%E2%80%93Bernstein_theorem" title="Schröder–Bernstein theorem">Schröder–Bernstein theorem</a></li>

<li><a href="Isomorphism" title="Isomorphism">Isomorphism</a></li>

<li><a href="G%C3%B6del_numbering" title="Gödel numbering">Gödel numbering</a></li>

<li><a href="Enumeration" title="Enumeration">Enumeration</a></li>

<li><a href="Large_cardinal" title="Large cardinal">Large cardinal</a>

<ul><li><a href="Inaccessible_cardinal" title="Inaccessible cardinal">inaccessible</a></li></ul></li>

<li><a href="Aleph_number" title="Aleph number">Aleph number</a></li>

<li><a href="Operation_(mathematics)" title="Operation (mathematics)">Operation</a>

<ul><li><a href="Binary_operation" title="Binary operation">binary</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Set theories</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel</a>

<ul><li><a href="Axiom_of_choice" title="Axiom of choice">axiom of choice</a></li>

<li><a href="Continuum_hypothesis" title="Continuum hypothesis">continuum hypothesis</a></li></ul></li>

<li><a href="General_set_theory" title="General set theory">General</a></li>

<li><a href="Kripke%E2%80%93Platek_set_theory" title="Kripke–Platek set theory">Kripke–Platek</a></li>

<li><a href="Morse%E2%80%93Kelley_set_theory" title="Morse–Kelley set theory">Morse–Kelley</a></li>

<li><a href="Naive_set_theory" title="Naive set theory">Naive</a></li>

<li><a href="New_Foundations" title="New Foundations">New Foundations</a></li>

<li><a href="Tarski%E2%80%93Grothendieck_set_theory" title="Tarski–Grothendieck set theory">Tarski–Grothendieck</a></li>

<li><a href="Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory" title="Von Neumann–Bernays–Gödel set theory">Von Neumann–Bernays–Gödel</a></li>

<li><a href="Ackermann_set_theory" title="Ackermann set theory">Ackermann</a></li>

<li><a href="Constructive_set_theory" title="Constructive set theory">Constructive</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Formal_system" title="Formal system">Formal systems</a> (<a href="List_of_formal_systems" title="List of formal systems">list</a>), <a href="Formal_language" title="Formal language">language</a> and <a href="Syntax_(logic)" title="Syntax (logic)">syntax</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><td colspan="2" class="navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Alphabet_(formal_languages)" title="Alphabet (formal languages)">Alphabet</a></li>

<li><a href="Arity" title="Arity">Arity</a></li>

<li><a href="Automata_theory" title="Automata theory">Automata</a></li>

<li><a href="Axiom_schema" title="Axiom schema">Axiom schema</a></li>

<li><a href="Expression_(mathematics)" title="Expression (mathematics)">Expression</a>

<ul><li><a href="Ground_expression" title="Ground expression">ground</a></li></ul></li>

<li><a href="Extension_by_new_constant_and_function_names" title="Extension by new constant and function names">Extension</a>

<ul><li><a href="Extension_by_definitions" class="mw-redirect" title="Extension by definitions">by definition</a></li>

<li><a href="Conservative_extension" title="Conservative extension">conservative</a></li></ul></li>

<li><a href="Finitary_relation" title="Finitary relation">Relation</a></li>

<li><a href="Formation_rule" title="Formation rule">Formation rule</a></li>

<li><a href="Formal_grammar" title="Formal grammar">Grammar</a></li>

<li><a href="Well-formed_formula" title="Well-formed formula">Formula</a>

<ul><li><a href="Atomic_formula" title="Atomic formula">atomic</a></li>

<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">closed</a></li>

<li><a href="Ground_formula" class="mw-redirect" title="Ground formula">ground</a></li>

<li><a href="Free_variables_and_bound_variables" title="Free variables and bound variables">Free/bound variable</a></li>

<li><a href="Formal_language" title="Formal language">Language</a></li>

<li><a href="Metalanguage" title="Metalanguage">Metalanguage</a></li>

<li><a href="Logical_connective" title="Logical connective">Logical connective</a>

<li><a href="Predicate_(mathematical_logic)" class="mw-redirect" title="Predicate (mathematical logic)">Predicate</a>

<ul><li><a href="Functional_predicate" title="Functional predicate">functional</a></li>

<li><a href="Predicate_variable" title="Predicate variable">variable</a></li>

<li><a href="Propositional_variable" title="Propositional variable">propositional variable</a></li></ul></li>

<li><a href="Formal_proof" title="Formal proof">Proof</a></li>

<li><a href="Quantifier_(logic)" title="Quantifier (logic)">Quantifier</a>

<li><a href="Sentence_(mathematical_logic)" title="Sentence (mathematical logic)">Sentence</a>

<ul><li><a href="Atomic_sentence" title="Atomic sentence">atomic</a></li>

<li><a href="Spectrum_of_a_sentence" title="Spectrum of a sentence">spectrum</a></li></ul></li>

<li><a href="Signature_(logic)" title="Signature (logic)">Signature</a></li>

<li><a href="String_(formal_languages)" class="mw-redirect" title="String (formal languages)">String</a></li>

<li><a href="Substitution_(logic)" title="Substitution (logic)">Substitution</a></li>

<li><a href="Symbol_(formal)" title="Symbol (formal)">Symbol</a>

<ul><li><a href="Uninterpreted_function" title="Uninterpreted function">function</a></li>

<li><a href="Logical_constant" title="Logical constant">logical/constant</a></li>

<li><a href="Non-logical_symbol" title="Non-logical symbol">non-logical</a></li>

<li><a href="Variable_(mathematics)" title="Variable (mathematics)">variable</a></li></ul></li>

<li><a href="Theory_(mathematical_logic)" title="Theory (mathematical logic)">Theory</a>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Example <a href="Axiomatic_system" title="Axiomatic system">axiomatic systems</a> (<a href="List_of_first-order_theories" title="List of first-order theories">list</a>)</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li>of <a href="True_arithmetic" title="True arithmetic">arithmetic</a>:

<ul><li><a href="Peano_axioms" title="Peano axioms">Peano</a></li>

<li><a href="Second-order_arithmetic" title="Second-order arithmetic">second-order</a></li>

<li><a href="Elementary_function_arithmetic" title="Elementary function arithmetic">elementary function</a></li>

<li><a href="Primitive_recursive_arithmetic" title="Primitive recursive arithmetic">primitive recursive</a></li>

<li><a href="Robinson_arithmetic" title="Robinson arithmetic">Robinson</a></li>

<li><a href="Skolem_arithmetic" title="Skolem arithmetic">Skolem</a></li></ul></li>

<li>of the <a href="Construction_of_the_real_numbers" title="Construction of the real numbers">real numbers</a>

<ul><li><a href="Tarski's_axiomatization_of_the_reals" title="Tarski's axiomatization of the reals">Tarski's axiomatization</a></li></ul></li>

<li>of <a href="Axiomatization_of_Boolean_algebras" class="mw-redirect" title="Axiomatization of Boolean algebras">Boolean algebras</a>

<ul><li><a href="Boolean_algebras_canonically_defined" title="Boolean algebras canonically defined">canonical</a></li>

<li><a href="Minimal_axioms_for_Boolean_algebra" title="Minimal axioms for Boolean algebra">minimal axioms</a></li></ul></li>

<li>of <a href="Foundations_of_geometry" title="Foundations of geometry">geometry</a>:

<ul><li><a href="Euclidean_geometry" title="Euclidean geometry">Euclidean</a>:

<ul><li><a href="Euclid's_Elements" title="Euclid's Elements">Elements</a></li>

<li><a href="Hilbert's_axioms" title="Hilbert's axioms">Hilbert's</a></li>

<li><a href="Tarski's_axioms" title="Tarski's axioms">Tarski's</a></li></ul></li>

<li><a href="Non-Euclidean_geometry" title="Non-Euclidean geometry">non-Euclidean</a></li></ul></li></ul>

<ul><li><a href="Principia_Mathematica" title="Principia Mathematica">Principia Mathematica</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Proof_theory" title="Proof theory">Proof theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Formal_proof" title="Formal proof">Formal proof</a></li>

<li><a href="Natural_deduction" title="Natural deduction">Natural deduction</a></li>

<li><a href="Logical_consequence" title="Logical consequence">Logical consequence</a></li>

<li><a href="Rule_of_inference" title="Rule of inference">Rule of inference</a></li>

<li><a href="Sequent_calculus" title="Sequent calculus">Sequent calculus</a></li>

<li><a href="Theorem" title="Theorem">Theorem</a></li>

<li><a href="Formal_system" title="Formal system">Systems</a>

<ul><li><a href="Axiomatic_system" title="Axiomatic system">axiomatic</a></li>

<li><a href="Deductive_system" class="mw-redirect" title="Deductive system">deductive</a></li>

<li><a href="Hilbert_system" title="Hilbert system">Hilbert</a>

<li><a href="Complete_theory" title="Complete theory">Complete theory</a></li>

<li><a href="Independence_(mathematical_logic)" title="Independence (mathematical logic)">Independence</a> (<a href="List_of_statements_independent_of_ZFC" title="List of statements independent of ZFC">from ZFC</a>)</li>

<li><a href="Proof_of_impossibility" title="Proof of impossibility">Proof of impossibility</a></li>

<li><a href="Ordinal_analysis" title="Ordinal analysis">Ordinal analysis</a></li>

<li><a href="Reverse_mathematics" title="Reverse mathematics">Reverse mathematics</a></li>

<li><a href="Self-verifying_theories" title="Self-verifying theories">Self-verifying theories</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Model_theory" title="Model theory">Model theory</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Interpretation_(logic)" title="Interpretation (logic)">Interpretation</a>

<ul><li><a href="Interpretation_function" class="mw-redirect" title="Interpretation function">function</a></li>

<li><a href="Interpretation_(model_theory)" title="Interpretation (model theory)">of models</a></li></ul></li>

<li><a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">Model</a>

<ul><li><a href="Elementary_equivalence" title="Elementary equivalence">equivalence</a></li>

<li><a href="Finite_model_theory" title="Finite model theory">finite</a></li>

<li><a href="Saturated_model" title="Saturated model">saturated</a></li>

<li><a href="Spectrum_of_a_theory" title="Spectrum of a theory">spectrum</a></li>

<li><a href="Substructure_(mathematics)" title="Substructure (mathematics)">submodel</a></li></ul></li>

<li><a href="Non-standard_model" title="Non-standard model">Non-standard model</a>

<ul><li><a href="Non-standard_model_of_arithmetic" title="Non-standard model of arithmetic">of arithmetic</a></li></ul></li>

<li><a href="Diagram_(mathematical_logic)" title="Diagram (mathematical logic)">Diagram</a>

<ul><li><a href="Elementary_diagram" title="Elementary diagram">elementary</a></li></ul></li>

<li><a href="Categorical_theory" title="Categorical theory">Categorical theory</a></li>

<li><a href="Model_complete_theory" title="Model complete theory">Model complete theory</a></li>

<li><a href="Satisfiability" title="Satisfiability">Satisfiability</a></li>

<li><a href="Semantics_of_logic" title="Semantics of logic">Semantics of logic</a></li>

<li><a href="Strength_(mathematical_logic)" title="Strength (mathematical logic)">Strength</a></li>

<li><a href="Theories_of_truth" class="mw-redirect" title="Theories of truth">Theories of truth</a>

<ul><li><a href="Semantic_theory_of_truth" title="Semantic theory of truth">semantic</a></li>

<li><a href="Tarski's_theory_of_truth" class="mw-redirect" title="Tarski's theory of truth">Tarski's</a></li>

<li><a href="Kripke's_theory_of_truth" class="mw-redirect" title="Kripke's theory of truth">Kripke's</a></li></ul></li>

<li><a href="T-schema" title="T-schema">T-schema</a></li>

<li><a href="Transfer_principle" title="Transfer principle">Transfer principle</a></li>

<li><a href="Truth_predicate" title="Truth predicate">Truth predicate</a></li>

<li><a href="Truth_value" title="Truth value">Truth value</a></li>

<li><a href="Ultraproduct" title="Ultraproduct">Ultraproduct</a></li>

<li><a href="Validity_(logic)" title="Validity (logic)">Validity</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computability_theory" title="Computability theory">Computability theory</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul>

<li><a href="Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a></li>

<li><a href="Computably_enumerable_set" title="Computably enumerable set">Computably enumerable</a></li>

<li><a href="Computable_function" title="Computable function">Computable function</a></li>

<li><a href="Computable_set" title="Computable set">Computable set</a></li>

<li><a href="Decision_problem" title="Decision problem">Decision problem</a>

<ul><li><a href="Decidability_(logic)" title="Decidability (logic)">decidable</a></li>

<li><a href="Undecidable_problem" title="Undecidable problem">undecidable</a></li>

<li><a href="P_versus_NP_problem" title="P versus NP problem">P versus NP problem</a></li></ul></li>

<li><a href="Kolmogorov_complexity" title="Kolmogorov complexity">Kolmogorov complexity</a></li>

<li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li>

<li><a href="Primitive_recursive_function" title="Primitive recursive function">Primitive recursive function</a></li>

<li><a href="Recursion" title="Recursion">Recursion</a></li>

<li><a href="Recursive_set" class="mw-redirect" title="Recursive set">Recursive set</a></li>

<li><a href="Turing_machine" title="Turing machine">Turing machine</a></li>

<li><a href="Type_theory" title="Type theory">Type theory</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Abstract_logic" title="Abstract logic">Abstract logic</a></li>

<li><a href="Algebraic_logic" title="Algebraic logic">Algebraic logic</a></li>

<li><a href="Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a></li>

<li><a href="Category_theory" title="Category theory">Category theory</a></li>

<li><a href="Concrete_category" title="Concrete category">Concrete</a>/<a href="Category_(mathematics)" title="Category (mathematics)">Abstract category</a></li>

<li><a href="Category_of_sets" title="Category of sets">Category of sets</a></li>

<li><a href="History_of_logic" title="History of logic">History of logic</a></li>

<li><a href="History_of_mathematical_logic" class="mw-redirect" title="History of mathematical logic">History of mathematical logic</a>

<ul><li><a href="Timeline_of_mathematical_logic" title="Timeline of mathematical logic">timeline</a></li></ul></li>

<li><a href="Logicism" title="Logicism">Logicism</a></li>

<li><a href="Mathematical_object" title="Mathematical object">Mathematical object</a></li>

<li><a href="Philosophy_of_mathematics" title="Philosophy of mathematics">Philosophy of mathematics</a></li>

<li><a href="Supertask" title="Supertask">Supertask</a></li></ul>

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div> <a href="Portal%3AMathematics" title="Portal:Mathematics">Mathematics portal</a></div></td></tr></tbody></table></div>

<div class="navbox-styles"></div><div role="navigation" class="navbox" aria-labelledby="Alonzo_Church56" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="Alonzo_Church56" style="font-size:114%;margin:0 4em"><a href="Alonzo_Church" title="Alonzo Church">Alonzo Church</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Notable ideas</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a>

<ul><li><a href="Simply_typed_lambda_calculus" title="Simply typed lambda calculus">Simply typed lambda calculus</a></li>

<li><a href="Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a></li>

</ul></li>

<li><a href="Frege%E2%80%93Church_ontology" title="Frege–Church ontology">Frege–Church ontology</a></li>

<li><a href="Church%E2%80%93Rosser_theorem" title="Church–Rosser theorem">Church–Rosser theorem</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Students</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Alan_Turing" title="Alan Turing">Alan Turing</a></li>

<li><a href="C._Anthony_Anderson" title="C. Anthony Anderson">C. Anthony Anderson</a></li>

<li><a href="Peter_B._Andrews" title="Peter B. Andrews">Peter Andrews</a></li>

<li><a href="George_Alfred_Barnard" title="George Alfred Barnard">George Alfred Barnard</a></li>

<li><a href="William_Boone_(mathematician)" title="William Boone (mathematician)">William Boone</a></li>

<li><a href="Martin_Davis_(mathematician)" title="Martin Davis (mathematician)">Martin Davis</a></li>

<li><a href="William_Bigelow_Easton" title="William Bigelow Easton">William Easton</a></li>

<li><a href="Alfred_Foster_(mathematician)" title="Alfred Foster (mathematician)">Alfred Foster</a></li>

<li><a href="Leon_Henkin" title="Leon Henkin">Leon Henkin</a></li>

<li><a href="John_George_Kemeny" class="mw-redirect" title="John George Kemeny">John George Kemeny</a></li>

<li><a href="Stephen_Cole_Kleene" title="Stephen Cole Kleene">Stephen Cole Kleene</a></li>

<li><a href="Simon_B._Kochen" title="Simon B. Kochen">Simon B. Kochen</a></li>

<li><a href="Maurice_L'Abb%C3%A9" title="Maurice L'Abbé">Maurice L'Abbé</a></li>

<li><a href="Michael_O._Rabin" title="Michael O. Rabin">Michael O. Rabin</a></li>

<li><a href="Nicholas_Rescher" title="Nicholas Rescher">Nicholas Rescher</a></li>

<li><a href="Hartley_Rogers%2C_Jr" class="mw-redirect" title="Hartley Rogers, Jr">Hartley Rogers, Jr</a></li>

<li><a href="J._Barkley_Rosser" title="J. Barkley Rosser">J. Barkley Rosser</a></li>

<li><a href="Dana_Scott" title="Dana Scott">Dana Scott</a></li>

<li><a href="Norman_Shapiro" title="Norman Shapiro">Norman Shapiro</a></li>

<li><a href="Raymond_Smullyan" title="Raymond Smullyan">Raymond Smullyan</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Institutions</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Princeton_University" title="Princeton University">Princeton University</a></li>

<li><a href="University_of_California%2C_Los_Angeles" title="University of California, Los Angeles">University of California, Los Angeles</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Family</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Alonzo_Church_(college_president)" title="Alonzo Church (college president)">Alonzo Church (college president)</a></li>

<li><a href="A._C._Croom" title="A. C. Croom">A. C. Croom</a></li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-08-08" href="https://en.wikipedia.org/wiki/?title=Church_encoding&oldid=1304813677">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>